Theorem simp33l 1157

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

Assertion

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

Proof of Theorem simp33l

Step	Hyp	Ref	Expression
1		simp3l 1058	. 2 |- ( ( ch /\ th /\ ( ph /\ ps ) ) -> ph )
2	1	3ad2ant3 1053	1 |- ( ( ta /\ et /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ph )

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  totprob  29333  cdleme19b  33942  cdleme19d  33944  cdleme19e  33945  cdleme20h  33954  cdleme20l2  33959  cdleme20m  33961  cdleme21d  33968  cdleme21e  33969  cdleme22e  33982  cdleme22f2  33985  cdleme22g  33986  cdleme26e  33997  cdleme28a  34008  cdleme28b  34009  cdleme37m  34100  cdleme39n  34104  cdlemeg46gfre  34170  cdlemg28a  34331  cdlemg28b  34341  cdlemk3  34471  cdlemk5a  34473  cdlemk6  34475  cdlemkuat  34504  cdlemkid2  34562