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  7007  oprabidw  7432  oprabid  7433  frxp  8106  smo11  8359  oaordex  8553  oaass  8556  omordi  8561  oeordsuc  8589  nnmordi  8626  nnmord  8627  nnaordex  8633  brecop  8800  findcard2OLD  9280  elfiun  9421  ordiso2  9506  ordtypelem7  9515  cantnf  9684  coftr  10264  domtriomlem  10433  prlem936  11038  zindd  12660  supxrun  13292  ccatopth2  14664  cau3lem  15298  climcau  15614  dvdsabseq  16253  divalglem8  16340  lcmf  16567  dirtr  18557  frgpnabllem1  19783  dprddisj2  19951  znrrg  21428  opnnei  22946  restntr  23008  lpcls  23190  comppfsc  23358  ufilmax  23733  ufileu  23745  flimfnfcls  23854  alexsubALTlem4  23876  qustgplem  23947  metrest  24355  caubl  25158  ulmcau  26248  ulmcn  26252  nodenselem8  27540  usgr2wlkneq  29482  erclwwlksym  29743  erclwwlktr  29744  erclwwlknsym  29792  erclwwlkntr  29793  sumdmdlem  32140  bnj1280  34520  fundmpss  35233  dfon2lem8  35257  ifscgr  35511  btwnconn1lem11  35564  btwnconn2  35569  finminlem  35693  opnrebl2  35696  fvineqsneq  36783  poimirlem21  36999  poimirlem26  37004  filbcmb  37098  seqpo  37105  mpobi123f  37520  mptbi12f  37524  ac6s6  37530  dia2dimlem12  40436  ntrk0kbimka  43279  truniALT  43791  onfrALTlem3  43794  ee223  43884  paireqne  46664  fmtnofac2lem  46721  setrec1lem4  47923