Theorem anandirs

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

	Ref	Expression
Hypothesis	anandirs.1	⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜏 )
Assertion	anandirs	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		anandirs.1	⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜏 )
2	1	an4s	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜒 ) ) → 𝜏 )
3	2	anabsan2	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜏 )