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  7015  oprabidw  7437  oprabid  7438  frxp  8109  smo11  8361  oaordex  8555  oaass  8558  omordi  8563  oeordsuc  8591  nnmordi  8628  nnmord  8629  nnaordex  8635  brecop  8801  findcard2OLD  9281  elfiun  9422  ordiso2  9507  ordtypelem7  9516  cantnf  9685  coftr  10265  domtriomlem  10434  prlem936  11039  zindd  12660  supxrun  13292  ccatopth2  14664  cau3lem  15298  climcau  15614  dvdsabseq  16253  divalglem8  16340  lcmf  16567  dirtr  18552  frgpnabllem1  19736  dprddisj2  19904  znrrg  21113  opnnei  22616  restntr  22678  lpcls  22860  comppfsc  23028  ufilmax  23403  ufileu  23415  flimfnfcls  23524  alexsubALTlem4  23546  qustgplem  23617  metrest  24025  caubl  24817  ulmcau  25899  ulmcn  25903  nodenselem8  27184  usgr2wlkneq  29003  erclwwlksym  29264  erclwwlktr  29265  erclwwlknsym  29313  erclwwlkntr  29314  sumdmdlem  31659  bnj1280  34020  fundmpss  34727  dfon2lem8  34751  ifscgr  35005  btwnconn1lem11  35058  btwnconn2  35063  finminlem  35192  opnrebl2  35195  fvineqsneq  36282  poimirlem21  36498  poimirlem26  36503  filbcmb  36597  seqpo  36604  mpobi123f  37019  mptbi12f  37023  ac6s6  37029  dia2dimlem12  39935  ntrk0kbimka  42776  truniALT  43288  onfrALTlem3  43291  ee223  43381  paireqne  46166  fmtnofac2lem  46223  setrec1lem4  47689