Theorem simpl32 1070

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

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965

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 371  df-3an 967

This theorem is referenced by:  tsmsxp  19854  ax5seg  23329  br8d  26086  br8  27703  cgrextend  28176  segconeq  28178  trisegint  28196  ifscgr  28212  cgrsub  28213  btwnxfr  28224  seglecgr12im  28278  segletr  28282  exatleN  33357  atbtwn  33399  3dim1  33420  3dim2  33421  2llnjaN  33519  4atlem10b  33558  4atlem11  33562  4atlem12  33565  2lplnj  33573  cdlemb  33747  paddasslem4  33776  pmodlem1  33799  4atex2  34030  trlval3  34140  arglem1N  34143  cdleme0moN  34178  cdleme17b  34240  cdleme20  34277  cdleme21j  34289  cdleme28c  34325  cdleme35h2  34410  cdleme38n  34417  cdlemg6c  34573  cdlemg6  34576  cdlemg7N  34579  cdlemg11a  34590  cdlemg12e  34600  cdlemg16  34610  cdlemg16ALTN  34611  cdlemg16zz  34613  cdlemg20  34638  cdlemg22  34640  cdlemg37  34642  cdlemg31d  34653  cdlemg29  34658  cdlemg33b  34660  cdlemg33  34664  cdlemg39  34669  cdlemg42  34682  cdlemk25-3  34857