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  7011  oprabidw  7443  oprabid  7444  frxp  8123  smo11  8352  oaordex  8544  oaass  8547  omordi  8552  oeordsuc  8581  nnmordi  8618  nnmord  8619  nnaordex  8625  brecop  8809  elfiun  9391  ordiso2  9478  ordtypelem7  9487  cantnf  9663  coftr  10258  domtriomlem  10427  prlem936  11033  zindd  12698  supxrun  13343  ccatopth2  14756  cau3lem  15408  climcau  15724  dvdsabseq  16372  divalglem8  16459  lcmf  16692  dirtr  18659  frgpnabllem1  19944  dprddisj2  20112  znrrg  21696  opnnei  23258  restntr  23320  lpcls  23502  comppfsc  23670  ufilmax  24045  ufileu  24057  flimfnfcls  24166  alexsubALTlem4  24188  qustgplem  24259  metrest  24662  caubl  25448  ulmcau  26539  ulmcn  26543  nodenselem8  27836  usgr2wlkneq  30086  erclwwlksym  30353  erclwwlktr  30354  erclwwlknsym  30402  erclwwlkntr  30403  sumdmdlem  32751  bnj1280  35389  antnestlaw2  36165  fundmpss  36240  dfon2lem8  36261  ifscgr  36517  btwnconn1lem11  36570  btwnconn2  36575  finminlem  36810  opnrebl2  36813  fvineqsneq  38039  poimirlem21  38273  poimirlem26  38278  filbcmb  38372  seqpo  38379  mpobi123f  38792  mptbi12f  38796  ac6s6  38802  dia2dimlem12  41830  aks6d1c1p2  42857  ntrk0kbimka  44748  truniALT  45233  onfrALTlem3  45236  ee223  45326  ormklocald  47573  paireqne  48243  fmtnofac2lem  48303  setrec1lem4  50451