Theorem simpl33 1080

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 974

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 369  df-3an 976

This theorem is referenced by:  ax5seglem3a  24650  ax5seg  24658  br8d  27900  br8  29969  cgrextend  30346  segconeq  30348  trisegint  30366  ifscgr  30382  cgrsub  30383  btwnxfr  30394  seglecgr12im  30448  segletr  30452  atbtwn  32463  4atlem10b  32622  4atlem11  32626  4atlem12  32629  2lplnj  32637  paddasslem4  32840  paddasslem7  32843  pmodlem1  32863  4atex2  33094  trlval3  33205  arglem1N  33208  cdleme0moN  33243  cdleme20  33343  cdleme21j  33355  cdleme28c  33391  cdleme38n  33483  cdlemg6c  33639  cdlemg6  33642  cdlemg7N  33645  cdlemg16  33676  cdlemg16ALTN  33677  cdlemg16zz  33679  cdlemg20  33704  cdlemg22  33706  cdlemg37  33708  cdlemg31d  33719  cdlemg29  33724  cdlemg33b  33726  cdlemg33  33730  cdlemg46  33754  cdlemk25-3  33923