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  7044  oprabidw  7482  oprabid  7483  frxp  8175  smo11  8410  oaordex  8604  oaass  8607  omordi  8612  oeordsuc  8641  nnmordi  8678  nnmord  8679  nnaordex  8685  brecop  8869  elfiun  9459  ordiso2  9546  ordtypelem7  9555  cantnf  9731  setrec1lem4  10008  coftr  10390  domtriomlem  10559  prlem936  11171  zindd  12840  supxrun  13486  ccatopth2  14908  cau3lem  15566  climcau  15882  dvdsabseq  16527  divalglem8  16614  lcmf  16852  dirtr  18826  frgpnabllem1  20138  dprddisj2  20306  znrrg  21926  opnnei  23493  restntr  23555  lpcls  23737  comppfsc  23906  ufilmax  24281  ufileu  24293  flimfnfcls  24402  alexsubALTlem4  24424  qustgplem  24495  metrest  24898  caubl  25684  ulmcau  26779  ulmcn  26783  nodenselem8  28105  usgr2wlkneq  30399  erclwwlksym  30669  erclwwlktr  30670  erclwwlknsym  30718  erclwwlkntr  30719  sumdmdlem  33077  bnj1280  35761  antnestlaw2  36665  fundmpss  36747  dfon2lem8  36767  ifscgr  37024  btwnconn1lem11  37077  btwnconn2  37082  finminlem  37321  opnrebl2  37324  fvineqsneq  38603  poimirlem21  38827  poimirlem26  38832  filbcmb  38940  seqpo  38947  mpobi123f  39360  mptbi12f  39364  ac6s6  39370  dia2dimlem12  42398  aks6d1c1p2  43425  ntrk0kbimka  45300  truniALT  45784  onfrALTlem3  45787  ee223  45877  cocanss2  46183  ormklocald  48159  paireqne  48866  fmtnofac2lem  48926