Theorem simpl33 1071

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 1026	. 2 |- ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) -> ch )
2	1	adantr 465	1 |- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ch )

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:  ax5seglem3a  23348  ax5seg  23356  br8d  26113  br8  27730  cgrextend  28203  segconeq  28205  trisegint  28223  ifscgr  28239  cgrsub  28240  btwnxfr  28251  seglecgr12im  28305  segletr  28309  atbtwn  33448  4atlem10b  33607  4atlem11  33611  4atlem12  33614  2lplnj  33622  paddasslem4  33825  paddasslem7  33828  pmodlem1  33848  4atex2  34079  trlval3  34189  arglem1N  34192  cdleme0moN  34227  cdleme20  34326  cdleme21j  34338  cdleme28c  34374  cdleme38n  34466  cdlemg6c  34622  cdlemg6  34625  cdlemg7N  34628  cdlemg16  34659  cdlemg16ALTN  34660  cdlemg16zz  34662  cdlemg20  34687  cdlemg22  34689  cdlemg37  34691  cdlemg31d  34702  cdlemg29  34707  cdlemg33b  34709  cdlemg33  34713  cdlemg46  34737  cdlemk25-3  34906