Theorem simp33l 1123

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

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

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 975

This theorem is referenced by:  totprob  28159  cdleme19b  35393  cdleme19d  35395  cdleme19e  35396  cdleme20h  35405  cdleme20l2  35410  cdleme20m  35412  cdleme21d  35419  cdleme21e  35420  cdleme22e  35433  cdleme22f2  35436  cdleme22g  35437  cdleme26e  35448  cdleme28a  35459  cdleme28b  35460  cdleme37m  35551  cdleme39n  35555  cdlemeg46gfre  35621  cdlemg28a  35782  cdlemg28b  35792  cdlemk3  35922  cdlemk5a  35924  cdlemk6  35926  cdlemkuat  35955  cdlemkid2  36013