Theorem mpdd 44

Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 16. (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 30	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpd 16	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpid  45  mpdi  46  syld  48  syl6c  71  mpteqb  7013  oprabidw  7451  oprabid  7452  frxp  8138  smo11  8372  oaordex  8566  oaass  8569  omordi  8574  oeordsuc  8603  nnmordi  8640  nnmord  8641  nnaordex  8647  brecop  8831  elfiun  9422  ordiso2  9509  ordtypelem7  9518  cantnf  9694  setrec1lem4  9971  coftr  10351  domtriomlem  10520  prlem936  11132  zindd  12800  supxrun  13446  ccatopth2  14866  cau3lem  15522  climcau  15838  dvdsabseq  16483  divalglem8  16570  lcmf  16808  dirtr  18776  frgpnabllem1  20087  dprddisj2  20255  znrrg  21871  opnnei  23438  restntr  23500  lpcls  23682  comppfsc  23851  ufilmax  24226  ufileu  24238  flimfnfcls  24347  alexsubALTlem4  24369  qustgplem  24440  metrest  24843  caubl  25629  ulmcau  26722  ulmcn  26726  nodenselem8  28048  usgr2wlkneq  30342  erclwwlksym  30612  erclwwlktr  30613  erclwwlknsym  30661  erclwwlkntr  30662  sumdmdlem  33020  bnj1280  35692  antnestlaw2  36499  fundmpss  36574  dfon2lem8  36594  ifscgr  36851  btwnconn1lem11  36904  btwnconn2  36909  finminlem  37148  opnrebl2  37151  fvineqsneq  38378  poimirlem21  38602  poimirlem26  38607  filbcmb  38717  seqpo  38724  mpobi123f  39137  mptbi12f  39141  ac6s6  39147  dia2dimlem12  42175  aks6d1c1p2  43202  ntrk0kbimka  45082  truniALT  45567  onfrALTlem3  45570  ee223  45660  cocanss2  45965  ormklocald  47929  paireqne  48636  fmtnofac2lem  48696