Theorem 3anandirs

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

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

Proof

Step	Hyp	Ref	Expression
1		3anandirs.1	⊢ ( ( ( 𝜑 ∧ 𝜃 ) ∧ ( 𝜓 ∧ 𝜃 ) ∧ ( 𝜒 ∧ 𝜃 ) ) → 𝜏 )
2		simpl1	⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) → 𝜑 )
3		simpr	⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) → 𝜃 )
4		simpl2	⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) → 𝜓 )
5		simpl3	⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) → 𝜒 )
6	2 3 4 3 5 3 1	syl222anc	⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ∧ 𝜃 ) → 𝜏 )