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  6764  oprabidw  7166  oprabid  7167  frxp  7803  smo11  7984  oaordex  8167  oaass  8170  omordi  8175  oeordsuc  8203  nnmordi  8240  nnmord  8241  nnaordex  8247  brecop  8373  findcard2  8742  elfiun  8878  ordiso2  8963  ordtypelem7  8972  cantnf  9140  coftr  9684  domtriomlem  9853  prlem936  10458  zindd  12071  supxrun  12697  ccatopth2  14070  cau3lem  14706  climcau  15019  dvdsabseq  15655  divalglem8  15741  lcmf  15967  dirtr  17838  frgpnabllem1  18986  dprddisj2  19154  znrrg  20257  opnnei  21725  restntr  21787  lpcls  21969  comppfsc  22137  ufilmax  22512  ufileu  22524  flimfnfcls  22633  alexsubALTlem4  22655  qustgplem  22726  metrest  23131  caubl  23912  ulmcau  24990  ulmcn  24994  usgr2wlkneq  27545  erclwwlksym  27806  erclwwlktr  27807  erclwwlknsym  27855  erclwwlkntr  27856  sumdmdlem  30201  bnj1280  32402  fundmpss  33122  dfon2lem8  33148  nodenselem8  33308  ifscgr  33618  btwnconn1lem11  33671  btwnconn2  33676  finminlem  33779  opnrebl2  33782  fvineqsneq  34829  poimirlem21  35078  poimirlem26  35083  filbcmb  35178  seqpo  35185  mpobi123f  35600  mptbi12f  35604  ac6s6  35610  dia2dimlem12  38371  ntrk0kbimka  40742  truniALT  41247  onfrALTlem3  41250  ee223  41340  paireqne  44028  fmtnofac2lem  44085  setrec1lem4  45220