Theorem axio

Definition of 'or' (intuitionistic logic axiom ax-io). (Contributed by Jim Kingdon, 21-May-2018.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \vee \chi \rightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\chi \rightarrow \psi) \)
Proof
jaob