This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem anandis

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

		Ref	Expression
	Hypothesis	anandis.1	$⊢ ((φ \land ψ) \land (φ \land χ)) \to τ$
	Assertion	anandis	$⊢ (φ \land (ψ \land χ)) \to τ$

Step	Hyp	Ref	Expression
1		anandis.1	$⊢ ((φ \land ψ) \land (φ \land χ)) \to τ$
2	1	an4s	$⊢ ((φ \land φ) \land (ψ \land χ)) \to τ$
3	2	anabsan	$⊢ (φ \land (ψ \land χ)) \to τ$