Theorem mpdd 43

Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 15. (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 29	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpd 15	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  44  mpdi  45  syld  47  syl6c  70  mpteqb  6962  oprabidw  7391  oprabid  7392  frxp  8070  smo11  8298  oaordex  8487  oaass  8490  omordi  8495  oeordsuc  8524  nnmordi  8561  nnmord  8562  nnaordex  8568  brecop  8751  elfiun  9337  ordiso2  9424  ordtypelem7  9433  cantnf  9606  coftr  10187  domtriomlem  10356  prlem936  10962  zindd  12597  supxrun  13235  ccatopth2  14644  cau3lem  15282  climcau  15598  dvdsabseq  16244  divalglem8  16331  lcmf  16564  dirtr  18529  frgpnabllem1  19806  dprddisj2  19974  znrrg  21524  opnnei  23068  restntr  23130  lpcls  23312  comppfsc  23480  ufilmax  23855  ufileu  23867  flimfnfcls  23976  alexsubALTlem4  23998  qustgplem  24069  metrest  24472  caubl  25268  ulmcau  26364  ulmcn  26368  nodenselem8  27663  usgr2wlkneq  29812  erclwwlksym  30079  erclwwlktr  30080  erclwwlknsym  30128  erclwwlkntr  30129  sumdmdlem  32476  bnj1280  35157  antnestlaw2  35867  fundmpss  35942  dfon2lem8  35963  ifscgr  36219  btwnconn1lem11  36272  btwnconn2  36277  finminlem  36493  opnrebl2  36496  fvineqsneq  37588  poimirlem21  37813  poimirlem26  37818  filbcmb  37912  seqpo  37919  mpobi123f  38334  mptbi12f  38338  ac6s6  38344  dia2dimlem12  41372  aks6d1c1p2  42400  ntrk0kbimka  44316  truniALT  44818  onfrALTlem3  44821  ee223  44911  ormklocald  47154  paireqne  47793  fmtnofac2lem  47850  setrec1lem4  49971