Theorem 3anandis

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

Hypothesis
3anandis.1
\( \vdash \varphi \wedge \psi \wedge \varphi \wedge \chi \wedge \varphi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \rightarrow \tau \)
Proof
l0
simpl
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \rightarrow \varphi \)
l1
simpr1
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \rightarrow \psi \)
l2
simpr2
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \rightarrow \chi \)
l3
simpr3
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \rightarrow \theta \)
3anandis.1
\( \vdash \varphi \wedge \psi \wedge \varphi \wedge \chi \wedge \varphi \wedge \theta \rightarrow \tau \)
syl222anc l0 l1 l0 l2 l0 l3 _