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  6969  oprabidw  7399  oprabid  7400  frxp  8078  smo11  8306  oaordex  8495  oaass  8498  omordi  8503  oeordsuc  8532  nnmordi  8569  nnmord  8570  nnaordex  8576  brecop  8759  elfiun  9345  ordiso2  9432  ordtypelem7  9441  cantnf  9614  coftr  10195  domtriomlem  10364  prlem936  10970  zindd  12605  supxrun  13243  ccatopth2  14652  cau3lem  15290  climcau  15606  dvdsabseq  16252  divalglem8  16339  lcmf  16572  dirtr  18537  frgpnabllem1  19814  dprddisj2  19982  znrrg  21532  opnnei  23076  restntr  23138  lpcls  23320  comppfsc  23488  ufilmax  23863  ufileu  23875  flimfnfcls  23984  alexsubALTlem4  24006  qustgplem  24077  metrest  24480  caubl  25276  ulmcau  26372  ulmcn  26376  nodenselem8  27671  usgr2wlkneq  29841  erclwwlksym  30108  erclwwlktr  30109  erclwwlknsym  30157  erclwwlkntr  30158  sumdmdlem  32505  bnj1280  35195  antnestlaw2  35905  fundmpss  35980  dfon2lem8  36001  ifscgr  36257  btwnconn1lem11  36310  btwnconn2  36315  finminlem  36531  opnrebl2  36534  fvineqsneq  37664  poimirlem21  37889  poimirlem26  37894  filbcmb  37988  seqpo  37995  mpobi123f  38410  mptbi12f  38414  ac6s6  38420  dia2dimlem12  41448  aks6d1c1p2  42476  ntrk0kbimka  44392  truniALT  44894  onfrALTlem3  44897  ee223  44987  ormklocald  47229  paireqne  47868  fmtnofac2lem  47925  setrec1lem4  50046