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  6894  oprabidw  7306  oprabid  7307  frxp  7967  smo11  8195  oaordex  8389  oaass  8392  omordi  8397  oeordsuc  8425  nnmordi  8462  nnmord  8463  nnaordex  8469  brecop  8599  findcard2OLD  9056  elfiun  9189  ordiso2  9274  ordtypelem7  9283  cantnf  9451  coftr  10029  domtriomlem  10198  prlem936  10803  zindd  12421  supxrun  13050  ccatopth2  14430  cau3lem  15066  climcau  15382  dvdsabseq  16022  divalglem8  16109  lcmf  16338  dirtr  18320  frgpnabllem1  19474  dprddisj2  19642  znrrg  20773  opnnei  22271  restntr  22333  lpcls  22515  comppfsc  22683  ufilmax  23058  ufileu  23070  flimfnfcls  23179  alexsubALTlem4  23201  qustgplem  23272  metrest  23680  caubl  24472  ulmcau  25554  ulmcn  25558  usgr2wlkneq  28124  erclwwlksym  28385  erclwwlktr  28386  erclwwlknsym  28434  erclwwlkntr  28435  sumdmdlem  30780  bnj1280  33000  fundmpss  33740  dfon2lem8  33766  nodenselem8  33894  ifscgr  34346  btwnconn1lem11  34399  btwnconn2  34404  finminlem  34507  opnrebl2  34510  fvineqsneq  35583  poimirlem21  35798  poimirlem26  35803  filbcmb  35898  seqpo  35905  mpobi123f  36320  mptbi12f  36324  ac6s6  36330  dia2dimlem12  39089  ntrk0kbimka  41649  truniALT  42161  onfrALTlem3  42164  ee223  42254  paireqne  44963  fmtnofac2lem  45020  setrec1lem4  46396