Theorem ndime-P3.6 171

Description: Natural Deduction: '→' Elimination Rule.

This rule is just Modus Ponens with an added context.

Hypotheses

Ref	Expression
ndime-P3.6.1	⊢ (𝛾 → 𝜑)
ndime-P3.6.2	⊢ (𝛾 → (𝜑 → 𝜓))

Assertion

Ref	Expression
ndime-P3.6	⊢ (𝛾 → 𝜓)

Proof of Theorem ndime-P3.6

Step	Hyp	Ref	Expression
1		ndime-P3.6.1	. 2 ⊢ (𝛾 → 𝜑)
2		ndime-P3.6.2	. 2 ⊢ (𝛾 → (𝜑 → 𝜓))
3	1, 2	mpt-P1.8.AC.2SH 58	1 ⊢ (𝛾 → 𝜓)

Syntax hints:   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-MP 14

This theorem is referenced by:  rcp-NDNEGI1  218  rcp-NDIME0  228  rcp-NDORE1  234  ndnegi-P3.3.CL  242  ndime-P3.6.CL  244  ndore-P3.12.CL  247  axL2-P3.22  254  mae-P3.23  257  syl-P3.24  259  rae-P3.26  263  imcomm-P3.27  265  trnsp-P3.31a  279  trnsp-P3.31b  282  trnsp-P3.31c  285  trnsp-P3.31d  288  mt-P3.32a  291  nmt-P3.32b  294  import-P3.34a  305  export-P3.34b  307  example-E3.2b  312  subandl-P3.42a-L1  338  suborl-P3.43a-L1  345  andasim-P3.46-L1  354  orasim-P3.48-L2  360  falseprofeliml-P4.7a  393  falseprofelimr-P4.7b  395  joinimandinc-P4.8a  397  joinimandres-P4.8b  400  joinimor-P4.8c  403  sepimandr-P4.9a  406  sepimorl-P4.9b  409  sepimorr-P4.9c  412  sepimandl-P4.9d  415  negbicancel-P4.11  419  negbicancelint-P4.14  424  falseie-P4.22b  445  oroverim-P4.28-L2  466  imoverim-P4.30-L1  476  imasor-P4.32-L1  485  imasandint-P4.33b  490  truthtbltbif-P4.39b  508  truthtblfbit-P4.39c  509  peirce-P4.40  511  exclmid2peirce-P4.41a  512  impime-P4  526  bimpf-P4  531  bimpr-P4  533  subneg2-P4  538  subiml2-P4  540  subimr2-P4  542  subimd2-P4  544  subbil2-P4  546  subbir2-P4  548  subbid2-P4  550  subandl2-P4  552  subandr2-P4  554  subandd2-P4  556  suborl2-P4  558  suborr2-P4  560  subord2-P4  562  alloverim-P5  588  eqsym-P5  627  eqtrns-P5  630  subeql-P5  632  eqmiddle-P6  708  ndexe-P6  825  exe-P7  955  qimeqex-P7-L2  1055