Theorem simpl32 1112

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

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  initoeu2lem2  15988  mulmarep1gsum2  19676  tsmsxp  21247  ax5seg  25047  br8d  28294  br8  30467  cgrextend  30846  segconeq  30848  trisegint  30866  ifscgr  30882  cgrsub  30883  btwnxfr  30894  seglecgr12im  30948  segletr  30952  exatleN  33040  atbtwn  33082  3dim1  33103  3dim2  33104  2llnjaN  33202  4atlem10b  33241  4atlem11  33245  4atlem12  33248  2lplnj  33256  cdlemb  33430  paddasslem4  33459  pmodlem1  33482  4atex2  33713  trlval3  33824  arglem1N  33827  cdleme0moN  33862  cdleme17b  33924  cdleme20  33962  cdleme21j  33974  cdleme28c  34010  cdleme35h2  34095  cdleme38n  34102  cdlemg6c  34258  cdlemg6  34261  cdlemg7N  34264  cdlemg11a  34275  cdlemg12e  34285  cdlemg16  34295  cdlemg16ALTN  34296  cdlemg16zz  34298  cdlemg20  34323  cdlemg22  34325  cdlemg37  34327  cdlemg31d  34338  cdlemg29  34343  cdlemg33b  34345  cdlemg33  34349  cdlemg39  34354  cdlemg42  34367  cdlemk25-3  34542