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 ⊢ (𝜑 → (𝜓 → 𝜃))

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  45  mpdi  46  syld  48  syl6c  71  mpteqb  7007  oprabidw  7439  oprabid  7440  frxp  8118  smo11  8347  oaordex  8539  oaass  8542  omordi  8547  oeordsuc  8576  nnmordi  8613  nnmord  8614  nnaordex  8620  brecop  8804  elfiun  9386  ordiso2  9473  ordtypelem7  9482  cantnf  9658  coftr  10253  domtriomlem  10422  prlem936  11028  zindd  12693  supxrun  13338  ccatopth2  14750  cau3lem  15402  climcau  15718  dvdsabseq  16367  divalglem8  16454  lcmf  16687  dirtr  18654  frgpnabllem1  19939  dprddisj2  20107  znrrg  21680  opnnei  23242  restntr  23304  lpcls  23486  comppfsc  23654  ufilmax  24029  ufileu  24041  flimfnfcls  24150  alexsubALTlem4  24172  qustgplem  24243  metrest  24646  caubl  25432  ulmcau  26520  ulmcn  26524  nodenselem8  27817  usgr2wlkneq  30042  erclwwlksym  30309  erclwwlktr  30310  erclwwlknsym  30358  erclwwlkntr  30359  sumdmdlem  32707  bnj1280  35349  antnestlaw2  36079  fundmpss  36154  dfon2lem8  36175  ifscgr  36431  btwnconn1lem11  36484  btwnconn2  36489  finminlem  36714  opnrebl2  36717  fvineqsneq  37941  poimirlem21  38175  poimirlem26  38180  filbcmb  38274  seqpo  38281  mpobi123f  38696  mptbi12f  38700  ac6s6  38706  dia2dimlem12  41734  aks6d1c1p2  42761  ntrk0kbimka  44650  truniALT  45135  onfrALTlem3  45138  ee223  45228  ormklocald  47475  paireqne  48142  fmtnofac2lem  48202  setrec1lem4  50346