Metamath Proof Explorer

Theorem 3anandis

Description: Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007)

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

Step	Hyp	Ref	Expression
1		3anandis.1	$⊢ ((φ \land ψ) \land (φ \land χ) \land (φ \land θ)) \to τ$
2		simpl	$⊢ (φ \land (ψ \land χ \land θ)) \to φ$
3		simpr1	$⊢ (φ \land (ψ \land χ \land θ)) \to ψ$
4		simpr2	$⊢ (φ \land (ψ \land χ \land θ)) \to χ$
5		simpr3	$⊢ (φ \land (ψ \land χ \land θ)) \to θ$
6	2 3 2 4 2 5 1	syl222anc	$⊢ (φ \land (ψ \land χ \land θ)) \to τ$