Theorem 3anandirs

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

Hypothesis
3anandirs.1
\( \vdash \varphi \wedge \theta \wedge \psi \wedge \theta \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge \theta \rightarrow \tau \)
Proof
l0
simpl1
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge \theta \rightarrow \varphi \)
l1
simpr
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge \theta \rightarrow \theta \)
l2
simpl2
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge \theta \rightarrow \psi \)
l3
simpl3
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge \theta \rightarrow \chi \)
3anandirs.1
\( \vdash \varphi \wedge \theta \wedge \psi \wedge \theta \wedge \chi \wedge \theta \rightarrow \tau \)
syl222anc l0 l1 l2 l1 l3 l1 _