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

Theorem simp2lr 1025
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 732 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 979 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  omeu  6787  4sqlem18  13285  vdwlem10  13313  mvrf1  16444  tsmsxp  18137  ax5seglem3  25774  btwnconn1lem1  25925  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem5  25929  btwnconn1lem6  25930  btwnconn1lem7  25931  linethru  25991  pellex  26788  expmordi  26900  lshpkrlem6  29598  athgt  29938  2llnjN  30049  dalaw  30368  cdlemb2  30523  4atexlemex6  30556  cdleme01N  30703  cdleme0ex2N  30706  cdleme7aa  30724  cdleme7e  30729  cdlemg33c0  31184  dihmeetlem3N  31788
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator