Theorem 3jao

Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \rightarrow \varphi \vee \chi \vee \theta \rightarrow \psi \)
Proof
l0
jao
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\chi \rightarrow \psi) \rightarrow \varphi \vee \chi \rightarrow \psi \)
l1
df-3or
\( \vdash \varphi \vee \chi \vee \theta \leftrightarrow \varphi \vee \chi \vee \theta \)
jao
\( \vdash (\varphi \vee \chi \rightarrow \psi) \rightarrow (\theta \rightarrow \psi) \rightarrow \varphi \vee \chi \vee \theta \rightarrow \psi \)
syl7bi l1 _
\( \vdash (\varphi \vee \chi \rightarrow \psi) \rightarrow (\theta \rightarrow \psi) \rightarrow \varphi \vee \chi \vee \theta \rightarrow \psi \)
syl6 l0 _
3imp _