Theorem simp33l 1115

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 1016	. 2 |- ( ( ch /\ th /\ ( ph /\ ps ) ) -> ph )
2	1	3ad2ant3 1011	1 |- ( ( ta /\ et /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ph )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965

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 185  df-an 371  df-3an 967

This theorem is referenced by:  totprob  26809  cdleme19b  33946  cdleme19d  33948  cdleme19e  33949  cdleme20h  33958  cdleme20l2  33963  cdleme20m  33965  cdleme21d  33972  cdleme21e  33973  cdleme22e  33986  cdleme22f2  33989  cdleme22g  33990  cdleme26e  34001  cdleme28a  34012  cdleme28b  34013  cdleme37m  34104  cdleme39n  34108  cdlemeg46gfre  34174  cdlemg28a  34335  cdlemg28b  34345  cdlemk3  34475  cdlemk5a  34477  cdlemk6  34479  cdlemkuat  34508  cdlemkid2  34566