Theorem simp121 1193

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

Assertion

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

Proof of Theorem simp121

Step	Hyp	Ref	Expression
1		simp21 1094	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ 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  axpasch  25821  exatleN  34690  ps-2b  34768  3atlem1  34769  3atlem2  34770  3atlem4  34772  3atlem5  34773  3atlem6  34774  2llnjaN  34852  4atlem12b  34897  2lplnja  34905  dalempea  34912  dath2  35023  lneq2at  35064  llnexchb2  35155  dalawlem1  35157  osumcllem7N  35248  lhpexle3lem  35297  cdleme26ee  35648  cdlemg34  36000  cdlemg36  36002  cdlemj1  36109  cdlemj2  36110  cdlemk23-3  36190  cdlemk25-3  36192  cdlemk26b-3  36193  cdlemk26-3  36194  cdlemk27-3  36195  cdleml3N  36266