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  11236  segconeu  24634  4atlem10  29795  lplncvrlvol2  29804  4atex  30265  4atex2-0cOLDN  30269  cdleme0moN  30414  cdleme16e  30471  cdleme17d1  30478  cdleme18d  30484  cdleme19d  30495  cdleme20f  30503  cdleme20g  30504  cdleme21ct  30518  cdleme22aa  30528  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme26e  30548  cdleme32e  30634  cdleme32f  30635  cdlemg4  30806  cdlemg18d  30870  cdlemg18  30871  cdlemg19a  30872  cdlemg19  30873  cdlemg21  30875  cdlemg33b0  30890  cdlemk5  31025  cdlemk6  31026  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemk21N  31062  cdlemk20  31063  cdlemk28-3  31097  cdlemk34  31099  cdlemkfid3N  31114  cdlemk55u1  31154
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