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	|- (ph -> ps)
mpd.2	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
mpd	|- (ph -> ch)

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 |- (ph -> ps)
2		mpd.2	. . 3 |- (ph -> (ps -> ch))
3	2	a2i 12	. 2 |- ((ph -> ps) -> (ph -> ch))
4	1, 3	ax-mp 5	1 |- (ph -> ch)

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  2743  vtoclgft  2906  sseldd  3275  ssneldd  3277  tpid3g  3832  preq12b  4128  iota5  4360  ssfin  4471  nnpw1ex  4485  tfin11  4494  tfinpw1  4495  evenodddisj  4517  sfin112  4530  sfindbl  4531  sfintfin  4533  sfinltfin  4536  vfin1cltv  4548  vfinspsslem1  4551  vinf  4556  nulnnn  4557  phi11lem1  4596  ffvelrn  5416  dffo4  5424  f1oiso2  5501  ov6g  5601  ovmpt2x  5713  trd  5922  antid  5930  connexd  5932  weds  5939  erref  5960  mapvalg  6010  mapsn  6027  enprmaplem3  6079  nenpw1pwlem2  6086  peano4nc  6151  ncspw1eu  6160  nntccl  6171  leconnnc  6219  tlecg  6231  ce2le  6234  addcdi  6251  ncslemuc  6256  nchoicelem17  6306  nchoicelem19  6308  nchoice  6309