Theorem anandis

Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004)

	Ref	Expression
Hypothesis	anandis.1	|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> ta )
Assertion	anandis	|- ( ( ph /\ ( ps /\ ch ) ) -> ta )

Proof

Step	Hyp	Ref	Expression
1		anandis.1	|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> ta )
2	1	an4s	|- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) -> ta )
3	2	anabsan	|- ( ( ph /\ ( ps /\ ch ) ) -> ta )