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

Metamath Proof Explorer

Theorem 3anandirs

Description: Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006)

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

Step	Hyp	Ref	Expression
1		3anandirs.1	$⊢ ((φ \land θ) \land (ψ \land θ) \land (χ \land θ)) \to τ$
2		simpl1	$⊢ ((φ \land ψ \land χ) \land θ) \to φ$
3		simpr	$⊢ ((φ \land ψ \land χ) \land θ) \to θ$
4		simpl2	$⊢ ((φ \land ψ \land χ) \land θ) \to ψ$
5		simpl3	$⊢ ((φ \land ψ \land χ) \land θ) \to χ$
6	2 3 4 3 5 3 1	syl222anc	$⊢ ((φ \land ψ \land χ) \land θ) \to τ$