Theorem simpl31 1142

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

Assertion

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

Proof of Theorem simpl31

Step	Hyp	Ref	Expression
1		simp31 1097	. 2 |- ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) -> ph )
2	1	adantr 481	1 |- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ax5seglem3a  25810  ax5seg  25818  uhgrwkspth  26651  usgr2wlkspth  26655  br8d  29422  br8  31646  nosupres  31853  cgrextend  32115  segconeq  32117  trisegint  32135  ifscgr  32151  cgrsub  32152  btwnxfr  32163  seglecgr12im  32217  segletr  32221  atbtwn  34732  3dim1  34753  2llnjaN  34852  4atlem10b  34891  4atlem11  34895  4atlem12  34898  2lplnj  34906  paddasslem4  35109  pmodlem1  35132  4atex2  35363  trlval3  35474  arglem1N  35477  cdleme0moN  35512  cdleme17b  35574  cdleme20  35612  cdleme21j  35624  cdleme28c  35660  cdleme35h2  35745  cdlemg6c  35908  cdlemg6  35911  cdlemg7N  35914  cdlemg8c  35917  cdlemg11a  35925  cdlemg11b  35930  cdlemg12e  35935  cdlemg16  35945  cdlemg16ALTN  35946  cdlemg16zz  35948  cdlemg20  35973  cdlemg22  35975  cdlemg37  35977  cdlemg31d  35988  cdlemg33b  35995  cdlemg33  35999  cdlemg39  36004  cdlemg42  36017  cdlemk25-3  36192  cdlemk33N  36197  cdlemk53b  36244