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  6876  oprabidw  7286  oprabid  7287  frxp  7938  smo11  8166  oaordex  8351  oaass  8354  omordi  8359  oeordsuc  8387  nnmordi  8424  nnmord  8425  nnaordex  8431  brecop  8557  findcard2OLD  8986  elfiun  9119  ordiso2  9204  ordtypelem7  9213  cantnf  9381  coftr  9960  domtriomlem  10129  prlem936  10734  zindd  12351  supxrun  12979  ccatopth2  14358  cau3lem  14994  climcau  15310  dvdsabseq  15950  divalglem8  16037  lcmf  16266  dirtr  18235  frgpnabllem1  19389  dprddisj2  19557  znrrg  20685  opnnei  22179  restntr  22241  lpcls  22423  comppfsc  22591  ufilmax  22966  ufileu  22978  flimfnfcls  23087  alexsubALTlem4  23109  qustgplem  23180  metrest  23586  caubl  24377  ulmcau  25459  ulmcn  25463  usgr2wlkneq  28025  erclwwlksym  28286  erclwwlktr  28287  erclwwlknsym  28335  erclwwlkntr  28336  sumdmdlem  30681  bnj1280  32900  fundmpss  33646  dfon2lem8  33672  nodenselem8  33821  ifscgr  34273  btwnconn1lem11  34326  btwnconn2  34331  finminlem  34434  opnrebl2  34437  fvineqsneq  35510  poimirlem21  35725  poimirlem26  35730  filbcmb  35825  seqpo  35832  mpobi123f  36247  mptbi12f  36251  ac6s6  36257  dia2dimlem12  39016  ntrk0kbimka  41538  truniALT  42050  onfrALTlem3  42053  ee223  42143  paireqne  44851  fmtnofac2lem  44908  setrec1lem4  46282