Theorem 3imp3i2an

An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.)

Hypotheses
3imp3i2an.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
3imp3i2an.2
\( \vdash \varphi \wedge \chi \rightarrow \tau \)
3imp3i2an.3
\( \vdash \theta \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \eta \)
Proof
l0
3imp3i2an.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
3imp3i2an.2
l2
3adant2 _
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \tau \)
3imp3i2an.3
\( \vdash \theta \wedge \tau \rightarrow \eta \)
syl2anc l0 l2 _