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  6943  oprabidw  7372  oprabid  7373  frxp  8051  smo11  8279  oaordex  8468  oaass  8471  omordi  8476  oeordsuc  8504  nnmordi  8541  nnmord  8542  nnaordex  8548  brecop  8729  elfiun  9309  ordiso2  9396  ordtypelem7  9405  cantnf  9578  coftr  10159  domtriomlem  10328  prlem936  10933  zindd  12569  supxrun  13210  ccatopth2  14619  cau3lem  15257  climcau  15573  dvdsabseq  16219  divalglem8  16306  lcmf  16539  dirtr  18503  frgpnabllem1  19780  dprddisj2  19948  znrrg  21497  opnnei  23030  restntr  23092  lpcls  23274  comppfsc  23442  ufilmax  23817  ufileu  23829  flimfnfcls  23938  alexsubALTlem4  23960  qustgplem  24031  metrest  24434  caubl  25230  ulmcau  26326  ulmcn  26330  nodenselem8  27625  usgr2wlkneq  29729  erclwwlksym  29993  erclwwlktr  29994  erclwwlknsym  30042  erclwwlkntr  30043  sumdmdlem  32390  bnj1280  35024  antnestlaw2  35728  fundmpss  35803  dfon2lem8  35824  ifscgr  36078  btwnconn1lem11  36131  btwnconn2  36136  finminlem  36352  opnrebl2  36355  fvineqsneq  37446  poimirlem21  37681  poimirlem26  37686  filbcmb  37780  seqpo  37787  mpobi123f  38202  mptbi12f  38206  ac6s6  38212  dia2dimlem12  41114  aks6d1c1p2  42142  ntrk0kbimka  44072  truniALT  44574  onfrALTlem3  44577  ee223  44667  ormklocald  46912  paireqne  47542  fmtnofac2lem  47599  setrec1lem4  49722