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  6987  oprabidw  7418  oprabid  7419  frxp  8105  smo11  8333  oaordex  8522  oaass  8525  omordi  8530  oeordsuc  8558  nnmordi  8595  nnmord  8596  nnaordex  8602  brecop  8783  elfiun  9381  ordiso2  9468  ordtypelem7  9477  cantnf  9646  coftr  10226  domtriomlem  10395  prlem936  11000  zindd  12635  supxrun  13276  ccatopth2  14682  cau3lem  15321  climcau  15637  dvdsabseq  16283  divalglem8  16370  lcmf  16603  dirtr  18561  frgpnabllem1  19803  dprddisj2  19971  znrrg  21475  opnnei  23007  restntr  23069  lpcls  23251  comppfsc  23419  ufilmax  23794  ufileu  23806  flimfnfcls  23915  alexsubALTlem4  23937  qustgplem  24008  metrest  24412  caubl  25208  ulmcau  26304  ulmcn  26308  nodenselem8  27603  usgr2wlkneq  29686  erclwwlksym  29950  erclwwlktr  29951  erclwwlknsym  29999  erclwwlkntr  30000  sumdmdlem  32347  bnj1280  35010  antnestlaw2  35679  fundmpss  35754  dfon2lem8  35778  ifscgr  36032  btwnconn1lem11  36085  btwnconn2  36090  finminlem  36306  opnrebl2  36309  fvineqsneq  37400  poimirlem21  37635  poimirlem26  37640  filbcmb  37734  seqpo  37741  mpobi123f  38156  mptbi12f  38160  ac6s6  38166  dia2dimlem12  41069  aks6d1c1p2  42097  ntrk0kbimka  44028  truniALT  44531  onfrALTlem3  44534  ee223  44624  ormklocald  46872  paireqne  47512  fmtnofac2lem  47569  setrec1lem4  49679