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  6757  4sqlem18  13250  vdwlem10  13278  mvrf1  16409  tsmsxp  18098  ax5seglem3  25577  btwnconn1lem1  25728  btwnconn1lem3  25730  btwnconn1lem4  25731  btwnconn1lem5  25732  btwnconn1lem6  25733  btwnconn1lem7  25734  linethru  25794  pellex  26582  expmordi  26694  lshpkrlem6  29281  athgt  29621  2llnjN  29732  dalaw  30051  cdlemb2  30206  4atexlemex6  30239  cdleme01N  30386  cdleme0ex2N  30389  cdleme7aa  30407  cdleme7e  30412  cdlemg33c0  30867  dihmeetlem3N  31471
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