Theorem simp22r 1181

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

Step	Hyp	Ref	Expression
1		simp2r 1088	. 2 |- ( ( ch /\ ( ph /\ ps ) /\ th ) -> ps )
2	1	3ad2ant2 1083	1 |- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) /\ et ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ax5seglem6  25814  segconeu  32118  3atlem2  34770  lplnexllnN  34850  lplncvrlvol2  34901  4atex  35362  cdleme3g  35521  cdleme3h  35522  cdleme11h  35553  cdleme20bN  35598  cdleme20c  35599  cdleme20f  35602  cdleme20g  35603  cdleme20j  35606  cdleme20l2  35609  cdleme20l  35610  cdleme21ct  35617  cdleme26e  35647  cdleme43fsv1snlem  35708  cdleme39n  35754  cdleme40m  35755  cdleme42k  35772  cdlemg6c  35908  cdlemg31d  35988  cdlemg33a  35994  cdlemg33c  35996  cdlemg33d  35997  cdlemg33e  35998  cdlemg33  35999  cdlemh  36105  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk20-2N  36180  cdlemk28-3  36196  cdlemk33N  36197  cdlemk34  36198  cdlemk39  36204  cdlemkyyN  36250