Theorem orimdi

Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)

Conclusion
\( \vdash \varphi \vee (\psi \rightarrow \chi) \leftrightarrow \varphi \vee \psi \rightarrow \varphi \vee \chi \)
Proof
l0
imdi
\( \vdash \neg \varphi \rightarrow \psi \rightarrow \chi \leftrightarrow (\neg \varphi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \chi \)
l1
df-or
\( \vdash \varphi \vee (\psi \rightarrow \chi) \leftrightarrow \neg \varphi \rightarrow \psi \rightarrow \chi \)
l2
df-or
df-or
imbi12i l2 _
\( \vdash \varphi \vee \psi \rightarrow \varphi \vee \chi \leftrightarrow (\neg \varphi \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \chi \)
3bitr4i l0 l1 _