Theorem 3jaob

Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011.) (Proof shortened by Hongxiu Chen, 29-Jun-2025.)

Conclusion
\( \vdash \varphi \vee \chi \vee \theta \rightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \)
Proof
l0
pm5.53
\( \vdash \varphi \vee \chi \vee \theta \rightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \)
df-3or
l2
imbi1i _
\( \vdash \varphi \vee \chi \vee \theta \rightarrow \psi \leftrightarrow \varphi \vee \chi \vee \theta \rightarrow \psi \)
df-3an
\( \vdash (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \wedge (\theta \rightarrow \psi) \)
3bitr4i l0 l2 _