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  7447  oprabid  7448  frxp  8124  smo11  8353  oaordex  8545  oaass  8548  omordi  8553  oeordsuc  8582  nnmordi  8619  nnmord  8620  nnaordex  8626  brecop  8810  elfiun  9393  ordiso2  9480  ordtypelem7  9489  cantnf  9665  coftr  10268  domtriomlem  10437  prlem936  11043  zindd  12708  supxrun  13353  ccatopth2  14771  cau3lem  15425  climcau  15741  dvdsabseq  16388  divalglem8  16475  lcmf  16708  dirtr  18675  frgpnabllem1  19966  dprddisj2  20134  znrrg  21744  opnnei  23306  restntr  23368  lpcls  23550  comppfsc  23718  ufilmax  24093  ufileu  24105  flimfnfcls  24214  alexsubALTlem4  24236  qustgplem  24307  metrest  24710  caubl  25496  ulmcau  26587  ulmcn  26591  nodenselem8  27884  usgr2wlkneq  30134  erclwwlksym  30401  erclwwlktr  30402  erclwwlknsym  30450  erclwwlkntr  30451  sumdmdlem  32799  bnj1280  35432  antnestlaw2  36197  fundmpss  36272  dfon2lem8  36293  ifscgr  36549  btwnconn1lem11  36602  btwnconn2  36607  finminlem  36862  opnrebl2  36865  fvineqsneq  38091  poimirlem21  38325  poimirlem26  38330  filbcmb  38424  seqpo  38431  mpobi123f  38844  mptbi12f  38848  ac6s6  38854  dia2dimlem12  41882  aks6d1c1p2  42909  ntrk0kbimka  44798  truniALT  45283  onfrALTlem3  45286  ee223  45376  ormklocald  47623  paireqne  48293  fmtnofac2lem  48353  setrec1lem4  50501