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  7046  oprabidw  7476  oprabid  7477  frxp  8163  smo11  8416  oaordex  8610  oaass  8613  omordi  8618  oeordsuc  8646  nnmordi  8683  nnmord  8684  nnaordex  8690  brecop  8864  elfiun  9495  ordiso2  9580  ordtypelem7  9589  cantnf  9758  coftr  10338  domtriomlem  10507  prlem936  11112  zindd  12740  supxrun  13374  ccatopth2  14761  cau3lem  15399  climcau  15715  dvdsabseq  16355  divalglem8  16442  lcmf  16674  dirtr  18667  frgpnabllem1  19910  dprddisj2  20078  znrrg  21602  opnnei  23142  restntr  23204  lpcls  23386  comppfsc  23554  ufilmax  23929  ufileu  23941  flimfnfcls  24050  alexsubALTlem4  24072  qustgplem  24143  metrest  24551  caubl  25354  ulmcau  26448  ulmcn  26452  nodenselem8  27745  usgr2wlkneq  29783  erclwwlksym  30044  erclwwlktr  30045  erclwwlknsym  30093  erclwwlkntr  30094  sumdmdlem  32441  bnj1280  34988  fundmpss  35722  dfon2lem8  35746  ifscgr  36000  btwnconn1lem11  36053  btwnconn2  36058  finminlem  36232  opnrebl2  36235  fvineqsneq  37327  poimirlem21  37550  poimirlem26  37555  filbcmb  37649  seqpo  37656  mpobi123f  38071  mptbi12f  38075  ac6s6  38081  dia2dimlem12  40981  aks6d1c1p2  42015  ntrk0kbimka  43942  truniALT  44453  onfrALTlem3  44456  ee223  44546  paireqne  47318  fmtnofac2lem  47375  setrec1lem4  48701