Theorem simp121 1123

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  ax5seglem3  23903  axpasch  23913  exatleN  34075  ps-2b  34153  3atlem1  34154  3atlem2  34155  3atlem4  34157  3atlem5  34158  3atlem6  34159  2llnjaN  34237  4atlem12b  34282  2lplnja  34290  dalempea  34297  dath2  34408  lneq2at  34449  llnexchb2  34540  dalawlem1  34542  osumcllem7N  34633  lhpexle3lem  34682  cdleme26ee  35031  cdlemg34  35383  cdlemg36  35385  cdlemj1  35492  cdlemj2  35493  cdlemk23-3  35573  cdlemk25-3  35575  cdlemk26b-3  35576  cdlemk26-3  35577  cdlemk27-3  35578  cdleml3N  35649