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

Theorem simp2lr 1056
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 754 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 1010 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  tfrlem5  6838  omeu  7023  4sqlem18  14022  vdwlem10  14050  mvrf1  17497  mdetuni0  18426  mdetmul  18428  tsmsxp  19728  ax5seglem3  23176  btwnconn1lem1  28117  btwnconn1lem3  28119  btwnconn1lem4  28120  btwnconn1lem5  28121  btwnconn1lem6  28122  btwnconn1lem7  28123  linethru  28183  pellex  29174  expmordi  29286  lshpkrlem6  32758  athgt  33098  2llnjN  33209  dalaw  33528  cdlemb2  33683  4atexlemex6  33716  cdleme01N  33863  cdleme0ex2N  33866  cdleme7aa  33884  cdleme7e  33889  cdlemg33c0  34344  dihmeetlem3N  34948
  Copyright terms: Public domain W3C validator