Theorem simp131 1196

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

Assertion

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

Proof of Theorem simp131

Step	Hyp	Ref	Expression
1		simp31 1097	. 2 |- ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ph )

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  exatleN  34690  3atlem1  34769  3atlem2  34770  3atlem5  34773  2llnjaN  34852  4atlem11b  34894  4atlem12b  34897  lplncvrlvol2  34901  dalemsea  34915  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  cdleml3N  36266