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  7014  oprabidw  7443  oprabid  7444  frxp  8132  smo11  8385  oaordex  8577  oaass  8580  omordi  8585  oeordsuc  8613  nnmordi  8650  nnmord  8651  nnaordex  8657  brecop  8831  elfiun  9451  ordiso2  9536  ordtypelem7  9545  cantnf  9714  coftr  10294  domtriomlem  10463  prlem936  11068  zindd  12701  supxrun  13339  ccatopth2  14736  cau3lem  15374  climcau  15688  dvdsabseq  16331  divalglem8  16418  lcmf  16651  dirtr  18615  frgpnabllem1  19858  dprddisj2  20026  znrrg  21537  opnnei  23073  restntr  23135  lpcls  23317  comppfsc  23485  ufilmax  23860  ufileu  23872  flimfnfcls  23981  alexsubALTlem4  24003  qustgplem  24074  metrest  24480  caubl  25277  ulmcau  26373  ulmcn  26377  nodenselem8  27671  usgr2wlkneq  29703  erclwwlksym  29967  erclwwlktr  29968  erclwwlknsym  30016  erclwwlkntr  30017  sumdmdlem  32364  bnj1280  34968  fundmpss  35701  dfon2lem8  35725  ifscgr  35979  btwnconn1lem11  36032  btwnconn2  36037  finminlem  36253  opnrebl2  36256  fvineqsneq  37347  poimirlem21  37582  poimirlem26  37587  filbcmb  37681  seqpo  37688  mpobi123f  38103  mptbi12f  38107  ac6s6  38113  dia2dimlem12  41011  aks6d1c1p2  42044  ntrk0kbimka  43990  truniALT  44494  onfrALTlem3  44497  ee223  44587  ormklocald  46822  paireqne  47432  fmtnofac2lem  47489  setrec1lem4  49193