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  24562  segconeu  24634  3atlem2  29673  lplnexllnN  29753  lplncvrlvol2  29804  4atex  30265  cdleme3g  30423  cdleme3h  30424  cdleme11h  30455  cdleme20bN  30499  cdleme20c  30500  cdleme20f  30503  cdleme20g  30504  cdleme20j  30507  cdleme20l2  30510  cdleme20l  30511  cdleme21ct  30518  cdleme26e  30548  cdleme43fsv1snlem  30609  cdleme39n  30655  cdleme40m  30656  cdleme42k  30673  cdlemg6c  30809  cdlemg31d  30889  cdlemg33a  30895  cdlemg33c  30897  cdlemg33d  30898  cdlemg33e  30899  cdlemg33  30900  cdlemh  31006  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk20-2N  31081  cdlemk28-3  31097  cdlemk33N  31098  cdlemk34  31099  cdlemk39  31105  cdlemkyyN  31151
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