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  7050  oprabidw  7481  oprabid  7482  frxp  8169  smo11  8422  oaordex  8616  oaass  8619  omordi  8624  oeordsuc  8652  nnmordi  8689  nnmord  8690  nnaordex  8696  brecop  8870  elfiun  9501  ordiso2  9586  ordtypelem7  9595  cantnf  9764  coftr  10344  domtriomlem  10513  prlem936  11118  zindd  12746  supxrun  13380  ccatopth2  14767  cau3lem  15405  climcau  15721  dvdsabseq  16363  divalglem8  16450  lcmf  16682  dirtr  18674  frgpnabllem1  19917  dprddisj2  20085  znrrg  21609  opnnei  23151  restntr  23213  lpcls  23395  comppfsc  23563  ufilmax  23938  ufileu  23950  flimfnfcls  24059  alexsubALTlem4  24081  qustgplem  24152  metrest  24560  caubl  25363  ulmcau  26458  ulmcn  26462  nodenselem8  27756  usgr2wlkneq  29794  erclwwlksym  30055  erclwwlktr  30056  erclwwlknsym  30104  erclwwlkntr  30105  sumdmdlem  32452  bnj1280  34998  fundmpss  35732  dfon2lem8  35756  ifscgr  36010  btwnconn1lem11  36063  btwnconn2  36068  finminlem  36286  opnrebl2  36289  fvineqsneq  37380  poimirlem21  37603  poimirlem26  37608  filbcmb  37702  seqpo  37709  mpobi123f  38124  mptbi12f  38128  ac6s6  38134  dia2dimlem12  41034  aks6d1c1p2  42068  ntrk0kbimka  44003  truniALT  44514  onfrALTlem3  44517  ee223  44607  paireqne  47387  fmtnofac2lem  47444  setrec1lem4  48788