Theorem simp132 1197

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 1098	. 2 |- ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) -> ps )
2	1	3ad2ant1 1082	1 |- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ps )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ax5seglem3  25811  3atlem1  34769  3atlem2  34770  3atlem5  34773  2llnjaN  34852  4atlem11b  34894  4atlem12b  34897  lplncvrlvol2  34901  dalemtea  34916  dath2  35023  cdlemblem  35079  dalawlem1  35157  lhpexle3lem  35297  4atexlemex6  35360  cdleme22f2  35635  cdleme22g  35636  cdlemg7aN  35913  cdlemg34  36000  cdlemj1  36109  cdlemk23-3  36190  cdlemk25-3  36192  cdlemk26b-3  36193