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

Theorem simp22r 1111
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 1018 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant2 1013 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970
This theorem is referenced by:  ax5seglem6  23906  segconeu  29224  3atlem2  34155  lplnexllnN  34235  lplncvrlvol2  34286  4atex  34747  cdleme3g  34905  cdleme3h  34906  cdleme11h  34937  cdleme20bN  34981  cdleme20c  34982  cdleme20f  34985  cdleme20g  34986  cdleme20j  34989  cdleme20l2  34992  cdleme20l  34993  cdleme21ct  35000  cdleme26e  35030  cdleme43fsv1snlem  35091  cdleme39n  35137  cdleme40m  35138  cdleme42k  35155  cdlemg6c  35291  cdlemg31d  35371  cdlemg33a  35377  cdlemg33c  35379  cdlemg33d  35380  cdlemg33e  35381  cdlemg33  35382  cdlemh  35488  cdlemk7u-2N  35559  cdlemk11u-2N  35560  cdlemk12u-2N  35561  cdlemk20-2N  35563  cdlemk28-3  35579  cdlemk33N  35580  cdlemk34  35581  cdlemk39  35587  cdlemkyyN  35633
  Copyright terms: Public domain W3C validator