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

Theorem simp22r 1077
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 984 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant2 979 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ax5seglem6  25873  segconeu  25945  3atlem2  30281  lplnexllnN  30361  lplncvrlvol2  30412  4atex  30873  cdleme3g  31031  cdleme3h  31032  cdleme11h  31063  cdleme20bN  31107  cdleme20c  31108  cdleme20f  31111  cdleme20g  31112  cdleme20j  31115  cdleme20l2  31118  cdleme20l  31119  cdleme21ct  31126  cdleme26e  31156  cdleme43fsv1snlem  31217  cdleme39n  31263  cdleme40m  31264  cdleme42k  31281  cdlemg6c  31417  cdlemg31d  31497  cdlemg33a  31503  cdlemg33c  31505  cdlemg33d  31506  cdlemg33e  31507  cdlemg33  31508  cdlemh  31614  cdlemk7u-2N  31685  cdlemk11u-2N  31686  cdlemk12u-2N  31687  cdlemk20-2N  31689  cdlemk28-3  31705  cdlemk33N  31706  cdlemk34  31707  cdlemk39  31713  cdlemkyyN  31759
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator