Theorem simp132 1124

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

Assertion

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

Proof of Theorem simp132

Step	Hyp	Ref	Expression
1		simp32 1025	. 2 |- ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) -> ps )
2	1	3ad2ant1 1009	1 |- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ps )

Syntax hints:   -> wi 4   /\ 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:  ax5seglem3  23324  3atlem1  33446  3atlem2  33447  3atlem5  33450  2llnjaN  33529  4atlem11b  33571  4atlem12b  33574  lplncvrlvol2  33578  dalemtea  33593  dath2  33700  cdlemblem  33756  dalawlem1  33834  lhpexle3lem  33974  4atexlemex6  34037  cdleme22f2  34310  cdleme22g  34311  cdlemg7aN  34588  cdlemg34  34675  cdlemj1  34784  cdlemk23-3  34865  cdlemk25-3  34867  cdlemk26b-3  34868