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  6967  oprabidw  7398  oprabid  7399  frxp  8076  smo11  8304  oaordex  8493  oaass  8496  omordi  8501  oeordsuc  8530  nnmordi  8567  nnmord  8568  nnaordex  8574  brecop  8757  elfiun  9343  ordiso2  9430  ordtypelem7  9439  cantnf  9614  coftr  10195  domtriomlem  10364  prlem936  10970  zindd  12630  supxrun  13268  ccatopth2  14679  cau3lem  15317  climcau  15633  dvdsabseq  16282  divalglem8  16369  lcmf  16602  dirtr  18568  frgpnabllem1  19848  dprddisj2  20016  znrrg  21545  opnnei  23085  restntr  23147  lpcls  23329  comppfsc  23497  ufilmax  23872  ufileu  23884  flimfnfcls  23993  alexsubALTlem4  24015  qustgplem  24086  metrest  24489  caubl  25275  ulmcau  26360  ulmcn  26364  nodenselem8  27655  usgr2wlkneq  29824  erclwwlksym  30091  erclwwlktr  30092  erclwwlknsym  30140  erclwwlkntr  30141  sumdmdlem  32489  bnj1280  35162  antnestlaw2  35874  fundmpss  35949  dfon2lem8  35970  ifscgr  36226  btwnconn1lem11  36279  btwnconn2  36284  finminlem  36500  opnrebl2  36503  fvineqsneq  37728  poimirlem21  37962  poimirlem26  37967  filbcmb  38061  seqpo  38068  mpobi123f  38483  mptbi12f  38487  ac6s6  38493  dia2dimlem12  41521  aks6d1c1p2  42548  ntrk0kbimka  44466  truniALT  44968  onfrALTlem3  44971  ee223  45061  ormklocald  47304  paireqne  47971  fmtnofac2lem  48031  setrec1lem4  50165