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  6994  oprabidw  7425  oprabid  7426  frxp  8114  smo11  8342  oaordex  8533  oaass  8536  omordi  8541  oeordsuc  8569  nnmordi  8606  nnmord  8607  nnaordex  8613  brecop  8787  elfiun  9399  ordiso2  9486  ordtypelem7  9495  cantnf  9664  coftr  10244  domtriomlem  10413  prlem936  11018  zindd  12651  supxrun  13289  ccatopth2  14692  cau3lem  15330  climcau  15644  dvdsabseq  16289  divalglem8  16376  lcmf  16609  dirtr  18567  frgpnabllem1  19809  dprddisj2  19977  znrrg  21481  opnnei  23013  restntr  23075  lpcls  23257  comppfsc  23425  ufilmax  23800  ufileu  23812  flimfnfcls  23921  alexsubALTlem4  23943  qustgplem  24014  metrest  24418  caubl  25215  ulmcau  26311  ulmcn  26315  nodenselem8  27610  usgr2wlkneq  29693  erclwwlksym  29957  erclwwlktr  29958  erclwwlknsym  30006  erclwwlkntr  30007  sumdmdlem  32354  bnj1280  35018  fundmpss  35751  dfon2lem8  35775  ifscgr  36029  btwnconn1lem11  36082  btwnconn2  36087  finminlem  36303  opnrebl2  36306  fvineqsneq  37397  poimirlem21  37632  poimirlem26  37637  filbcmb  37731  seqpo  37738  mpobi123f  38153  mptbi12f  38157  ac6s6  38163  dia2dimlem12  41061  aks6d1c1p2  42089  ntrk0kbimka  44000  truniALT  44503  onfrALTlem3  44506  ee223  44596  ormklocald  46845  paireqne  47467  fmtnofac2lem  47524  setrec1lem4  49556