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  6441  oprabid  6822  frxp  7438  smo11  7614  oaordex  7792  oaass  7795  omordi  7800  oeordsuc  7828  nnmordi  7865  nnmord  7866  nnaordex  7872  brecop  7992  findcard2  8356  elfiun  8492  ordiso2  8576  ordtypelem7  8585  cantnf  8754  coftr  9297  domtriomlem  9466  prlem936  10071  zindd  11680  supxrun  12351  ccatopth2  13680  cau3lem  14302  climcau  14609  dvdsabseq  15244  divalglem8  15331  lcmf  15554  dirtr  17444  frgpnabllem1  18483  dprddisj2  18646  znrrg  20129  opnnei  21145  restntr  21207  lpcls  21389  comppfsc  21556  ufilmax  21931  ufileu  21943  flimfnfcls  22052  alexsubALTlem4  22074  qustgplem  22144  metrest  22549  caubl  23325  ulmcau  24369  ulmcn  24373  usgr2wlkneq  26887  erclwwlksym  27171  erclwwlktr  27172  erclwwlknsym  27228  erclwwlkntr  27229  sumdmdlem  29617  bnj1280  31426  fundmpss  32002  dfon2lem8  32031  nodenselem8  32178  ifscgr  32488  btwnconn1lem11  32541  btwnconn2  32546  finminlem  32649  opnrebl2  32653  poimirlem21  33763  poimirlem26  33768  filbcmb  33867  seqpo  33875  mpt2bi123f  34303  mptbi12f  34307  ac6s6  34312  dia2dimlem12  36885  ntrk0kbimka  38863  truniALT  39276  onfrALTlem3  39284  ee223  39384  fmtnofac2lem  42008  setrec1lem4  42965