Theorem simpl32 1076

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

Assertion

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

Proof of Theorem simpl32

Step	Hyp	Ref	Expression
1		simp32 1031	. 2 |- ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) -> ps )
2	1	adantr 463	1 |- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ps )

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

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 973

This theorem is referenced by:  initoeu2lem2  15493  mulmarep1gsum2  19243  tsmsxp  20823  ax5seg  24443  br8d  27678  br8  29426  cgrextend  29886  segconeq  29888  trisegint  29906  ifscgr  29922  cgrsub  29923  btwnxfr  29934  seglecgr12im  29988  segletr  29992  exatleN  35525  atbtwn  35567  3dim1  35588  3dim2  35589  2llnjaN  35687  4atlem10b  35726  4atlem11  35730  4atlem12  35733  2lplnj  35741  cdlemb  35915  paddasslem4  35944  pmodlem1  35967  4atex2  36198  trlval3  36309  arglem1N  36312  cdleme0moN  36347  cdleme17b  36409  cdleme20  36447  cdleme21j  36459  cdleme28c  36495  cdleme35h2  36580  cdleme38n  36587  cdlemg6c  36743  cdlemg6  36746  cdlemg7N  36749  cdlemg11a  36760  cdlemg12e  36770  cdlemg16  36780  cdlemg16ALTN  36781  cdlemg16zz  36783  cdlemg20  36808  cdlemg22  36810  cdlemg37  36812  cdlemg31d  36823  cdlemg29  36828  cdlemg33b  36830  cdlemg33  36834  cdlemg39  36839  cdlemg42  36852  cdlemk25-3  37027