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

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

Proof of Theorem simp22r
StepHypRef Expression
1 simp2r 982 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant2 977 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seglem6  24634  segconeu  24706  3atlem2  30295  lplnexllnN  30375  lplncvrlvol2  30426  4atex  30887  cdleme3g  31045  cdleme3h  31046  cdleme11h  31077  cdleme20bN  31121  cdleme20c  31122  cdleme20f  31125  cdleme20g  31126  cdleme20j  31129  cdleme20l2  31132  cdleme20l  31133  cdleme21ct  31140  cdleme26e  31170  cdleme43fsv1snlem  31231  cdleme39n  31277  cdleme40m  31278  cdleme42k  31295  cdlemg6c  31431  cdlemg31d  31511  cdlemg33a  31517  cdlemg33c  31519  cdlemg33d  31520  cdlemg33e  31521  cdlemg33  31522  cdlemh  31628  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk20-2N  31703  cdlemk28-3  31719  cdlemk33N  31720  cdlemk34  31721  cdlemk39  31727  cdlemkyyN  31773
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