Theorem anandirs

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

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

Proof

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