Theorem mpdd 42

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  43  mpdi  44  syld  46  syl6c  68  mpteqb  6207  oprabid  6576  frxp  7174  smo11  7348  oaordex  7525  oaass  7528  omordi  7533  oeordsuc  7561  nnmordi  7598  nnmord  7599  nnaordex  7605  brecop  7727  findcard2  8085  elfiun  8219  ordiso2  8303  ordtypelem7  8312  cantnf  8473  coftr  8978  domtriomlem  9147  prlem936  9748  zindd  11354  supxrun  12018  ccatopth2  13323  cau3lem  13942  climcau  14249  dvdsabseq  14873  divalglem8  14961  lcmf  15184  dirtr  17059  frgpnabllem1  18099  dprddisj2  18261  znrrg  19733  opnnei  20734  restntr  20796  lpcls  20978  comppfsc  21145  ufilmax  21521  ufileu  21533  flimfnfcls  21642  alexsubALTlem4  21664  qustgplem  21734  metrest  22139  caubl  22914  ulmcau  23953  ulmcn  23957  usgranloopv  25907  erclwwlksym  26342  erclwwlktr  26343  erclwwlknsym  26354  erclwwlkntr  26355  sumdmdlem  28661  bnj1280  30342  fundmpss  30910  dfon2lem8  30939  nodenselem7  31086  nodenselem8  31087  ifscgr  31321  btwnconn1lem11  31374  btwnconn2  31379  finminlem  31482  opnrebl2  31486  poimirlem21  32600  poimirlem26  32605  filbcmb  32705  seqpo  32713  mpt2bi123f  33141  mptbi12f  33145  ac6s6  33150  dia2dimlem12  35382  ntrk0kbimka  37357  truniALT  37772  onfrALTlem3  37780  ee223  37880  fmtnofac2lem  40018  usgr2wlkneq  40962  elwspths2on  41163  erclwwlkssym  41242  erclwwlkstr  41243  erclwwlksnsym  41254  erclwwlksntr  41255  setrec1lem4  42236