Theorem 3anandis

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

	Ref	Expression
Hypothesis	3anandis.1	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜑 ∧ 𝜃 ) ) → 𝜏 )
Assertion	3anandis	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		3anandis.1	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜑 ∧ 𝜒 ) ∧ ( 𝜑 ∧ 𝜃 ) ) → 𝜏 )
2		simpl	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜑 )
3		simpr1	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜓 )
4		simpr2	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜒 )
5		simpr3	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜃 )
6	2 3 2 4 2 5 1	syl222anc	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) ) → 𝜏 )