MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpdd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mpdd.1 . 2 (𝜑 → (𝜓𝜒))
2 mpdd.2 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32a2d 29 . 2 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
41, 3mpd 15 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
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  6783  oprabidw  7179  oprabid  7180  frxp  7811  smo11  7992  oaordex  8174  oaass  8177  omordi  8182  oeordsuc  8210  nnmordi  8247  nnmord  8248  nnaordex  8254  brecop  8380  findcard2  8747  elfiun  8883  ordiso2  8968  ordtypelem7  8977  cantnf  9145  coftr  9684  domtriomlem  9853  prlem936  10458  zindd  12072  supxrun  12699  ccatopth2  14069  cau3lem  14704  climcau  15017  dvdsabseq  15653  divalglem8  15741  lcmf  15967  dirtr  17836  frgpnabllem1  18913  dprddisj2  19081  znrrg  20628  opnnei  21644  restntr  21706  lpcls  21888  comppfsc  22056  ufilmax  22431  ufileu  22443  flimfnfcls  22552  alexsubALTlem4  22574  qustgplem  22644  metrest  23049  caubl  23826  ulmcau  24898  ulmcn  24902  usgr2wlkneq  27451  erclwwlksym  27713  erclwwlktr  27714  erclwwlknsym  27763  erclwwlkntr  27764  sumdmdlem  30109  bnj1280  32176  fundmpss  32893  dfon2lem8  32919  nodenselem8  33079  ifscgr  33389  btwnconn1lem11  33442  btwnconn2  33447  finminlem  33550  opnrebl2  33553  fvineqsneq  34562  poimirlem21  34780  poimirlem26  34785  filbcmb  34883  seqpo  34890  mpobi123f  35308  mptbi12f  35312  ac6s6  35318  dia2dimlem12  38078  ntrk0kbimka  40254  truniALT  40740  onfrALTlem3  40743  ee223  40833  paireqne  43505  fmtnofac2lem  43562  setrec1lem4  44625
  Copyright terms: Public domain W3C validator