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

Theorem simp21r 1073
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21r  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 980 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant2 977 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  modexp  11252  segconeu  24706  4atlem10  30417  lplncvrlvol2  30426  4atex  30887  4atex2-0cOLDN  30891  cdleme0moN  31036  cdleme16e  31093  cdleme17d1  31100  cdleme18d  31106  cdleme19d  31117  cdleme20f  31125  cdleme20g  31126  cdleme21ct  31140  cdleme22aa  31150  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme26e  31170  cdleme32e  31256  cdleme32f  31257  cdlemg4  31428  cdlemg18d  31492  cdlemg18  31493  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg33b0  31512  cdlemk5  31647  cdlemk6  31648  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemk21N  31684  cdlemk20  31685  cdlemk28-3  31719  cdlemk34  31721  cdlemkfid3N  31736  cdlemk55u1  31776
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