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	⊢ (𝜑 → (𝜓 → 𝜒))
mpdd.2	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
mpdd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem mpdd

Step	Hyp	Ref	Expression
1		mpdd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mpdd.2	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpd 15	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  6969  oprabidw  7400  oprabid  7401  frxp  8082  smo11  8310  oaordex  8499  oaass  8502  omordi  8507  oeordsuc  8535  nnmordi  8572  nnmord  8573  nnaordex  8579  brecop  8760  elfiun  9357  ordiso2  9444  ordtypelem7  9453  cantnf  9622  coftr  10202  domtriomlem  10371  prlem936  10976  zindd  12611  supxrun  13252  ccatopth2  14658  cau3lem  15297  climcau  15613  dvdsabseq  16259  divalglem8  16346  lcmf  16579  dirtr  18537  frgpnabllem1  19779  dprddisj2  19947  znrrg  21451  opnnei  22983  restntr  23045  lpcls  23227  comppfsc  23395  ufilmax  23770  ufileu  23782  flimfnfcls  23891  alexsubALTlem4  23913  qustgplem  23984  metrest  24388  caubl  25184  ulmcau  26280  ulmcn  26284  nodenselem8  27579  usgr2wlkneq  29659  erclwwlksym  29923  erclwwlktr  29924  erclwwlknsym  29972  erclwwlkntr  29973  sumdmdlem  32320  bnj1280  34983  antnestlaw2  35652  fundmpss  35727  dfon2lem8  35751  ifscgr  36005  btwnconn1lem11  36058  btwnconn2  36063  finminlem  36279  opnrebl2  36282  fvineqsneq  37373  poimirlem21  37608  poimirlem26  37613  filbcmb  37707  seqpo  37714  mpobi123f  38129  mptbi12f  38133  ac6s6  38139  dia2dimlem12  41042  aks6d1c1p2  42070  ntrk0kbimka  44001  truniALT  44504  onfrALTlem3  44507  ee223  44597  ormklocald  46845  paireqne  47485  fmtnofac2lem  47542  setrec1lem4  49652