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  6806  oprabidw  7213  oprabid  7214  frxp  7858  smo11  8042  oaordex  8227  oaass  8230  omordi  8235  oeordsuc  8263  nnmordi  8300  nnmord  8301  nnaordex  8307  brecop  8433  findcard2OLD  8846  elfiun  8979  ordiso2  9064  ordtypelem7  9073  cantnf  9241  coftr  9785  domtriomlem  9954  prlem936  10559  zindd  12176  supxrun  12804  ccatopth2  14180  cau3lem  14816  climcau  15132  dvdsabseq  15770  divalglem8  15857  lcmf  16086  dirtr  17974  frgpnabllem1  19124  dprddisj2  19292  znrrg  20396  opnnei  21883  restntr  21945  lpcls  22127  comppfsc  22295  ufilmax  22670  ufileu  22682  flimfnfcls  22791  alexsubALTlem4  22813  qustgplem  22884  metrest  23289  caubl  24072  ulmcau  25154  ulmcn  25158  usgr2wlkneq  27709  erclwwlksym  27970  erclwwlktr  27971  erclwwlknsym  28019  erclwwlkntr  28020  sumdmdlem  30365  bnj1280  32583  fundmpss  33326  dfon2lem8  33352  nodenselem8  33549  ifscgr  34001  btwnconn1lem11  34054  btwnconn2  34059  finminlem  34162  opnrebl2  34165  fvineqsneq  35238  poimirlem21  35453  poimirlem26  35458  filbcmb  35553  seqpo  35560  mpobi123f  35975  mptbi12f  35979  ac6s6  35985  dia2dimlem12  38744  ntrk0kbimka  41235  truniALT  41739  onfrALTlem3  41742  ee223  41832  paireqne  44544  fmtnofac2lem  44601  setrec1lem4  45896