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  7018  oprabidw  7440  oprabid  7441  frxp  8112  smo11  8364  oaordex  8558  oaass  8561  omordi  8566  oeordsuc  8594  nnmordi  8631  nnmord  8632  nnaordex  8638  brecop  8804  findcard2OLD  9284  elfiun  9425  ordiso2  9510  ordtypelem7  9519  cantnf  9688  coftr  10268  domtriomlem  10437  prlem936  11042  zindd  12663  supxrun  13295  ccatopth2  14667  cau3lem  15301  climcau  15617  dvdsabseq  16256  divalglem8  16343  lcmf  16570  dirtr  18555  frgpnabllem1  19741  dprddisj2  19909  znrrg  21121  opnnei  22624  restntr  22686  lpcls  22868  comppfsc  23036  ufilmax  23411  ufileu  23423  flimfnfcls  23532  alexsubALTlem4  23554  qustgplem  23625  metrest  24033  caubl  24825  ulmcau  25907  ulmcn  25911  nodenselem8  27194  usgr2wlkneq  29013  erclwwlksym  29274  erclwwlktr  29275  erclwwlknsym  29323  erclwwlkntr  29324  sumdmdlem  31671  bnj1280  34031  fundmpss  34738  dfon2lem8  34762  ifscgr  35016  btwnconn1lem11  35069  btwnconn2  35074  finminlem  35203  opnrebl2  35206  fvineqsneq  36293  poimirlem21  36509  poimirlem26  36514  filbcmb  36608  seqpo  36615  mpobi123f  37030  mptbi12f  37034  ac6s6  37040  dia2dimlem12  39946  ntrk0kbimka  42790  truniALT  43302  onfrALTlem3  43305  ee223  43395  paireqne  46179  fmtnofac2lem  46236  setrec1lem4  47735