Theorem simp121 1138

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

Syntax hints:   -> wi 4   /\ w3a 983

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 189  df-an 373  df-3an 985

This theorem is referenced by:  ax5seglem3  24953  axpasch  24963  exatleN  32932  ps-2b  33010  3atlem1  33011  3atlem2  33012  3atlem4  33014  3atlem5  33015  3atlem6  33016  2llnjaN  33094  4atlem12b  33139  2lplnja  33147  dalempea  33154  dath2  33265  lneq2at  33306  llnexchb2  33397  dalawlem1  33399  osumcllem7N  33490  lhpexle3lem  33539  cdleme26ee  33890  cdlemg34  34242  cdlemg36  34244  cdlemj1  34351  cdlemj2  34352  cdlemk23-3  34432  cdlemk25-3  34434  cdlemk26b-3  34435  cdlemk26-3  34436  cdlemk27-3  34437  cdleml3N  34508