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

Theorem simp22r 1125
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 1032 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant2 1027 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  ax5seglem6  24810  segconeu  30563  3atlem2  32761  lplnexllnN  32841  lplncvrlvol2  32892  4atex  33353  cdleme3g  33512  cdleme3h  33513  cdleme11h  33544  cdleme20bN  33589  cdleme20c  33590  cdleme20f  33593  cdleme20g  33594  cdleme20j  33597  cdleme20l2  33600  cdleme20l  33601  cdleme21ct  33608  cdleme26e  33638  cdleme43fsv1snlem  33699  cdleme39n  33745  cdleme40m  33746  cdleme42k  33763  cdlemg6c  33899  cdlemg31d  33979  cdlemg33a  33985  cdlemg33c  33987  cdlemg33d  33988  cdlemg33e  33989  cdlemg33  33990  cdlemh  34096  cdlemk7u-2N  34167  cdlemk11u-2N  34168  cdlemk12u-2N  34169  cdlemk20-2N  34171  cdlemk28-3  34187  cdlemk33N  34188  cdlemk34  34189  cdlemk39  34195  cdlemkyyN  34241
  Copyright terms: Public domain W3C validator