Theorem simp21r 1179

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp21r	|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) /\ et ) -> ps )

Proof of Theorem simp21r

Step	Hyp	Ref	Expression
1		simp1r 1086	. 2 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )
2	1	3ad2ant2 1083	1 |- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ 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:  modexp  12999  segconeu  32118  4atlem10  34892  lplncvrlvol2  34901  4atex  35362  4atex2-0cOLDN  35366  cdleme0moN  35512  cdleme16e  35569  cdleme17d1  35576  cdleme18d  35582  cdleme19d  35594  cdleme20f  35602  cdleme20g  35603  cdleme21ct  35617  cdleme22aa  35627  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme26e  35647  cdleme32e  35733  cdleme32f  35734  cdlemg4  35905  cdlemg18d  35969  cdlemg18  35970  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg33b0  35989  cdlemk5  36124  cdlemk6  36125  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemk21N  36161  cdlemk20  36162  cdlemk28-3  36196  cdlemk34  36198  cdlemkfid3N  36213  cdlemk55u1  36253