Theorem mpd 14

Description: A modus ponens deduction. A translation of natural deduction rule → E (→ elimination). (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpd.1	⊢ (φ → ψ)
mpd.2	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
mpd	⊢ (φ → χ)

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 ⊢ (φ → ψ)
2		mpd.2	. . 3 ⊢ (φ → (ψ → χ))
3	2	a2i 12	. 2 ⊢ ((φ → ψ) → (φ → χ))
4	1, 3	ax-mp 5	1 ⊢ (φ → χ)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-2 7

This theorem is referenced by:  syl  15  mpi  16  id  19  mpcom  32  mpdd  36  mp2d  41  pm2.43i  43  syl3c  57  pm2.21dd  99  mt2d  109  mt3d  117  mt4d  130  mpbid  201  mpbird  223  mpjaod  370  jcai  522  mp2and  660  mp3and  1280  exlimddv  1638  exlimdd  1889  eqrdav  2352  rexlimddv  2742  vtoclgft  2905  sseldd  3274  ssneldd  3276  tpid3g  3831  preq12b  4127  iota5  4359  ssfin  4470  nnpw1ex  4484  tfin11  4493  tfinpw1  4494  evenodddisj  4516  sfin112  4529  sfindbl  4530  sfintfin  4532  sfinltfin  4535  vfin1cltv  4547  vfinspsslem1  4550  vinf  4555  nulnnn  4556  phi11lem1  4595  ffvelrn  5415  dffo4  5423  f1oiso2  5500  ov6g  5600  ovmpt2x  5712  trd  5921  antid  5929  connexd  5931  weds  5938  erref  5959  mapvalg  6009  mapsn  6026  enprmaplem3  6078  nenpw1pwlem2  6085  peano4nc  6150  ncspw1eu  6159  nntccl  6170  leconnnc  6218  tlecg  6230  ce2le  6233  addcdi  6250  ncslemuc  6255  nchoicelem17  6305  nchoicelem19  6307  nchoice  6308