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

Theorem simp2lr 1023
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 731 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ps )
213ad2ant2 977 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  omeu  6599  4sqlem18  13025  vdwlem10  13053  mvrf1  16186  tsmsxp  17853  ax5seglem3  24631  btwnconn1lem1  24782  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem7  24788  linethru  24848  pellex  27023  expmordi  27135  lshpkrlem6  29927  athgt  30267  2llnjN  30378  dalaw  30697  cdlemb2  30852  4atexlemex6  30885  cdleme01N  31032  cdleme0ex2N  31035  cdleme7aa  31053  cdleme7e  31058  cdlemg33c0  31513  dihmeetlem3N  32117
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator