Theorem mpdd 43

Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 15. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mpdd.1	|- ( ph -> ( ps -> ch ) )
mpdd.2	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
mpdd	|- ( ph -> ( ps -> th ) )

Proof of Theorem mpdd

Step	Hyp	Ref	Expression
1		mpdd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		mpdd.2	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	a2d 29	. 2 |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )
4	1, 3	mpd 15	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  mpid  44  mpdi  45  syld  47  syl6c  70  mpteqb  6299  oprabid  6677  frxp  7287  smo11  7461  oaordex  7638  oaass  7641  omordi  7646  oeordsuc  7674  nnmordi  7711  nnmord  7712  nnaordex  7718  brecop  7840  findcard2  8200  elfiun  8336  ordiso2  8420  ordtypelem7  8429  cantnf  8590  coftr  9095  domtriomlem  9264  prlem936  9869  zindd  11478  supxrun  12146  ccatopth2  13471  cau3lem  14094  climcau  14401  dvdsabseq  15035  divalglem8  15123  lcmf  15346  dirtr  17236  frgpnabllem1  18276  dprddisj2  18438  znrrg  19914  opnnei  20924  restntr  20986  lpcls  21168  comppfsc  21335  ufilmax  21711  ufileu  21723  flimfnfcls  21832  alexsubALTlem4  21854  qustgplem  21924  metrest  22329  caubl  23106  ulmcau  24149  ulmcn  24153  usgr2wlkneq  26652  elwspths2on  26853  erclwwlkssym  26935  erclwwlkstr  26936  erclwwlksnsym  26947  erclwwlksntr  26948  sumdmdlem  29277  bnj1280  31088  fundmpss  31664  dfon2lem8  31695  nodenselem8  31841  ifscgr  32151  btwnconn1lem11  32204  btwnconn2  32209  finminlem  32312  opnrebl2  32316  poimirlem21  33430  poimirlem26  33435  filbcmb  33535  seqpo  33543  mpt2bi123f  33971  mptbi12f  33975  ac6s6  33980  dia2dimlem12  36364  ntrk0kbimka  38337  truniALT  38751  onfrALTlem3  38759  ee223  38859  fmtnofac2lem  41480  setrec1lem4  42437