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  6583  4sqlem18  13009  vdwlem10  13037  mvrf1  16170  tsmsxp  17837  ax5seglem3  24559  btwnconn1lem1  24710  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem7  24716  linethru  24776  pellex  26920  expmordi  27032  lshpkrlem6  29305  athgt  29645  2llnjN  29756  dalaw  30075  cdlemb2  30230  4atexlemex6  30263  cdleme01N  30410  cdleme0ex2N  30413  cdleme7aa  30431  cdleme7e  30436  cdlemg33c0  30891  dihmeetlem3N  31495
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