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  6955  oprabidw  7387  oprabid  7388  frxp  8066  smo11  8294  oaordex  8483  oaass  8486  omordi  8491  oeordsuc  8520  nnmordi  8557  nnmord  8558  nnaordex  8564  brecop  8747  elfiun  9333  ordiso2  9420  ordtypelem7  9429  cantnf  9605  coftr  10186  domtriomlem  10355  prlem936  10961  zindd  12621  supxrun  13259  ccatopth2  14670  cau3lem  15308  climcau  15624  dvdsabseq  16273  divalglem8  16360  lcmf  16593  dirtr  18559  frgpnabllem1  19839  dprddisj2  20007  znrrg  21540  opnnei  23103  restntr  23165  lpcls  23347  comppfsc  23515  ufilmax  23890  ufileu  23902  flimfnfcls  24011  alexsubALTlem4  24033  qustgplem  24104  metrest  24507  caubl  25293  ulmcau  26378  ulmcn  26382  nodenselem8  27673  usgr2wlkneq  29842  erclwwlksym  30109  erclwwlktr  30110  erclwwlknsym  30158  erclwwlkntr  30159  sumdmdlem  32507  bnj1280  35202  antnestlaw2  35920  fundmpss  35995  dfon2lem8  36016  ifscgr  36272  btwnconn1lem11  36325  btwnconn2  36330  finminlem  36546  opnrebl2  36549  fvineqsneq  37774  poimirlem21  38008  poimirlem26  38013  filbcmb  38107  seqpo  38114  mpobi123f  38529  mptbi12f  38533  ac6s6  38539  dia2dimlem12  41567  aks6d1c1p2  42594  ntrk0kbimka  44483  truniALT  44985  onfrALTlem3  44988  ee223  45078  ormklocald  47319  paireqne  47986  fmtnofac2lem  48046  setrec1lem4  50180