Theorem olc

Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)

Conclusion

\( \vdash \varphi \rightarrow \psi \vee \varphi \)

Proof

ax-1

orrd _