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  7006  oprabidw  7444  oprabid  7445  frxp  8124  smo11  8353  oaordex  8545  oaass  8548  omordi  8553  oeordsuc  8582  nnmordi  8619  nnmord  8620  nnaordex  8626  brecop  8810  elfiun  9400  ordiso2  9487  ordtypelem7  9496  cantnf  9672  coftr  10275  domtriomlem  10444  prlem936  11056  zindd  12722  supxrun  13368  ccatopth2  14786  cau3lem  15442  climcau  15758  dvdsabseq  16403  divalglem8  16490  lcmf  16723  dirtr  18690  frgpnabllem1  20000  dprddisj2  20168  znrrg  21778  opnnei  23345  restntr  23407  lpcls  23589  comppfsc  23758  ufilmax  24133  ufileu  24145  flimfnfcls  24254  alexsubALTlem4  24276  qustgplem  24347  metrest  24750  caubl  25536  ulmcau  26631  ulmcn  26635  nodenselem8  27927  usgr2wlkneq  30221  erclwwlksym  30491  erclwwlktr  30492  erclwwlknsym  30540  erclwwlkntr  30541  sumdmdlem  32899  bnj1280  35529  antnestlaw2  36271  fundmpss  36346  dfon2lem8  36367  ifscgr  36624  btwnconn1lem11  36677  btwnconn2  36682  finminlem  36937  opnrebl2  36940  fvineqsneq  38166  poimirlem21  38390  poimirlem26  38395  filbcmb  38490  seqpo  38497  mpobi123f  38910  mptbi12f  38914  ac6s6  38920  dia2dimlem12  41948  aks6d1c1p2  42975  ntrk0kbimka  44879  truniALT  45364  onfrALTlem3  45367  ee223  45457  ormklocald  47704  paireqne  48411  fmtnofac2lem  48471  setrec1lem4  50616