Theorem simp312 1105

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

Assertion

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

Proof of Theorem simp312

Step	Hyp	Ref	Expression
1		simp12 988	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ps )
2	1	3ad2ant3 980	1 |- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ps )

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  dalemrot  30139  dalem-cly  30153  dath2  30219  cdleme26e  30841  cdleme38m  30945  cdleme38n  30946  cdleme39n  30948  cdlemg28b  31185  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemk7u  31352  cdlemk11u  31353  cdlemk12u  31354  cdlemk22  31375  cdlemk23-3  31384  cdlemk25-3  31386

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938