Theorem simpl33 1090

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

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 984

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 189  df-an 373  df-3an 986

This theorem is referenced by:  ax5seglem3a  24953  ax5seg  24961  br8d  28211  br8  30389  cgrextend  30768  segconeq  30770  trisegint  30788  ifscgr  30804  cgrsub  30805  btwnxfr  30816  seglecgr12im  30870  segletr  30874  atbtwn  33005  4atlem10b  33164  4atlem11  33168  4atlem12  33171  2lplnj  33179  paddasslem4  33382  paddasslem7  33385  pmodlem1  33405  4atex2  33636  trlval3  33747  arglem1N  33750  cdleme0moN  33785  cdleme20  33885  cdleme21j  33897  cdleme28c  33933  cdleme38n  34025  cdlemg6c  34181  cdlemg6  34184  cdlemg7N  34187  cdlemg16  34218  cdlemg16ALTN  34219  cdlemg16zz  34221  cdlemg20  34246  cdlemg22  34248  cdlemg37  34250  cdlemg31d  34261  cdlemg29  34266  cdlemg33b  34268  cdlemg33  34272  cdlemg46  34296  cdlemk25-3  34465