Theorem simp123 1195

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

Assertion

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

Proof of Theorem simp123

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

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  2llnjN  34853  4atlem12b  34897  2lplnja  34905  2lplnj  34906  dalemrea  34914  dath2  35023  lneq2at  35064  osumcllem7N  35248  cdleme26ee  35648  cdlemg35  36001  cdlemg36  36002  cdlemj1  36109  cdlemk23-3  36190  cdlemk25-3  36192  cdlemk26b-3  36193  cdlemk27-3  36195  cdlemk28-3  36196  cdleml3N  36266