Theorem simpl32 1090

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

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

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 987

This theorem is referenced by:  initoeu2lem2  15910  mulmarep1gsum2  19599  tsmsxp  21169  ax5seg  24968  br8d  28218  br8  30396  cgrextend  30775  segconeq  30777  trisegint  30795  ifscgr  30811  cgrsub  30812  btwnxfr  30823  seglecgr12im  30877  segletr  30881  exatleN  32969  atbtwn  33011  3dim1  33032  3dim2  33033  2llnjaN  33131  4atlem10b  33170  4atlem11  33174  4atlem12  33177  2lplnj  33185  cdlemb  33359  paddasslem4  33388  pmodlem1  33411  4atex2  33642  trlval3  33753  arglem1N  33756  cdleme0moN  33791  cdleme17b  33853  cdleme20  33891  cdleme21j  33903  cdleme28c  33939  cdleme35h2  34024  cdleme38n  34031  cdlemg6c  34187  cdlemg6  34190  cdlemg7N  34193  cdlemg11a  34204  cdlemg12e  34214  cdlemg16  34224  cdlemg16ALTN  34225  cdlemg16zz  34227  cdlemg20  34252  cdlemg22  34254  cdlemg37  34256  cdlemg31d  34267  cdlemg29  34272  cdlemg33b  34274  cdlemg33  34278  cdlemg39  34283  cdlemg42  34296  cdlemk25-3  34471