MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2lr Structured version   Unicode version

Theorem simp2lr 1073
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp2lr  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )

Proof of Theorem simp2lr
StepHypRef Expression
1 simplr 760 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 1027 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  tfrlem5  7053  omeu  7241  4sqlem18OLD  14849  4sqlem18  14855  vdwlem10  14883  mvrf1  18592  mdetuni0  19588  mdetmul  19590  tsmsxp  21111  ax5seglem3  24903  btwnconn1lem1  30803  btwnconn1lem3  30805  btwnconn1lem4  30806  btwnconn1lem5  30807  btwnconn1lem6  30808  btwnconn1lem7  30809  linethru  30869  lshpkrlem6  32593  athgt  32933  2llnjN  33044  dalaw  33363  cdlemb2  33518  4atexlemex6  33551  cdleme01N  33699  cdleme0ex2N  33702  cdleme7aa  33720  cdleme7e  33725  cdlemg33c0  34181  dihmeetlem3N  34785  pellex  35592  expmordi  35708
  Copyright terms: Public domain W3C validator