Theorem simpl33 1113

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

Assertion

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

Proof of Theorem simpl33

Step	Hyp	Ref	Expression
1		simp33 1068	. 2 |- ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) -> ch )
2	1	adantr 472	1 |- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ch )

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:  ax5seglem3a  25039  ax5seg  25047  br8d  28294  br8  30467  cgrextend  30846  segconeq  30848  trisegint  30866  ifscgr  30882  cgrsub  30883  btwnxfr  30894  seglecgr12im  30948  segletr  30952  atbtwn  33082  4atlem10b  33241  4atlem11  33245  4atlem12  33248  2lplnj  33256  paddasslem4  33459  paddasslem7  33462  pmodlem1  33482  4atex2  33713  trlval3  33824  arglem1N  33827  cdleme0moN  33862  cdleme20  33962  cdleme21j  33974  cdleme28c  34010  cdleme38n  34102  cdlemg6c  34258  cdlemg6  34261  cdlemg7N  34264  cdlemg16  34295  cdlemg16ALTN  34296  cdlemg16zz  34298  cdlemg20  34323  cdlemg22  34325  cdlemg37  34327  cdlemg31d  34338  cdlemg29  34343  cdlemg33b  34345  cdlemg33  34349  cdlemg46  34373  cdlemk25-3  34542