Theorem ex3

Apply ex to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction. (Contributed by Alan Sare, 22-Apr-2018.)

Hypothesis

ex3.1

\( \vdash \varphi \wedge \psi \wedge \chi \wedge \theta \rightarrow \tau \)

Conclusion

\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \rightarrow \tau \)

Proof

ex3.1

ex _

3impa _