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  6957  oprabidw  7386  oprabid  7387  frxp  8065  smo11  8293  oaordex  8482  oaass  8485  omordi  8490  oeordsuc  8518  nnmordi  8555  nnmord  8556  nnaordex  8562  brecop  8743  elfiun  9325  ordiso2  9412  ordtypelem7  9421  cantnf  9594  coftr  10175  domtriomlem  10344  prlem936  10949  zindd  12584  supxrun  13222  ccatopth2  14631  cau3lem  15269  climcau  15585  dvdsabseq  16231  divalglem8  16318  lcmf  16551  dirtr  18516  frgpnabllem1  19793  dprddisj2  19961  znrrg  21511  opnnei  23055  restntr  23117  lpcls  23299  comppfsc  23467  ufilmax  23842  ufileu  23854  flimfnfcls  23963  alexsubALTlem4  23985  qustgplem  24056  metrest  24459  caubl  25255  ulmcau  26351  ulmcn  26355  nodenselem8  27650  usgr2wlkneq  29755  erclwwlksym  30022  erclwwlktr  30023  erclwwlknsym  30071  erclwwlkntr  30072  sumdmdlem  32419  bnj1280  35104  antnestlaw2  35808  fundmpss  35883  dfon2lem8  35904  ifscgr  36160  btwnconn1lem11  36213  btwnconn2  36218  finminlem  36434  opnrebl2  36437  fvineqsneq  37529  poimirlem21  37754  poimirlem26  37759  filbcmb  37853  seqpo  37860  mpobi123f  38275  mptbi12f  38279  ac6s6  38285  dia2dimlem12  41247  aks6d1c1p2  42275  ntrk0kbimka  44196  truniALT  44698  onfrALTlem3  44701  ee223  44791  ormklocald  47034  paireqne  47673  fmtnofac2lem  47730  setrec1lem4  49851