Theorem 3jaao

Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Garrett Katz, 16-Jun-2026.)

Hypotheses
3jaao.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
3jaao.2
\( \vdash \theta \rightarrow \tau \rightarrow \chi \)
3jaao.3
\( \vdash \eta \rightarrow \zeta \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \theta \wedge \eta \rightarrow \psi \vee \tau \vee \zeta \rightarrow \chi \)
Proof
l0
3jaao.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l1
3jaao.2
\( \vdash \theta \rightarrow \tau \rightarrow \chi \)
l2
3jaao.3
\( \vdash \eta \rightarrow \zeta \rightarrow \chi \)
3jao
\( \vdash (\psi \rightarrow \chi) \wedge (\tau \rightarrow \chi) \wedge (\zeta \rightarrow \chi) \rightarrow \psi \vee \tau \vee \zeta \rightarrow \chi \)
syl3an l0 l1 l2 _