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  6961  oprabidw  7391  oprabid  7392  frxp  8069  smo11  8297  oaordex  8486  oaass  8489  omordi  8494  oeordsuc  8523  nnmordi  8560  nnmord  8561  nnaordex  8567  brecop  8750  elfiun  9336  ordiso2  9423  ordtypelem7  9432  cantnf  9605  coftr  10186  domtriomlem  10355  prlem936  10961  zindd  12621  supxrun  13259  ccatopth2  14670  cau3lem  15308  climcau  15624  dvdsabseq  16273  divalglem8  16360  lcmf  16593  dirtr  18559  frgpnabllem1  19839  dprddisj2  20007  znrrg  21555  opnnei  23095  restntr  23157  lpcls  23339  comppfsc  23507  ufilmax  23882  ufileu  23894  flimfnfcls  24003  alexsubALTlem4  24025  qustgplem  24096  metrest  24499  caubl  25285  ulmcau  26373  ulmcn  26377  nodenselem8  27669  usgr2wlkneq  29839  erclwwlksym  30106  erclwwlktr  30107  erclwwlknsym  30155  erclwwlkntr  30156  sumdmdlem  32504  bnj1280  35178  antnestlaw2  35890  fundmpss  35965  dfon2lem8  35986  ifscgr  36242  btwnconn1lem11  36295  btwnconn2  36300  finminlem  36516  opnrebl2  36519  fvineqsneq  37742  poimirlem21  37976  poimirlem26  37981  filbcmb  38075  seqpo  38082  mpobi123f  38497  mptbi12f  38501  ac6s6  38507  dia2dimlem12  41535  aks6d1c1p2  42562  ntrk0kbimka  44484  truniALT  44986  onfrALTlem3  44989  ee223  45079  ormklocald  47320  paireqne  47983  fmtnofac2lem  48043  setrec1lem4  50177