Theorem orim1i

Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)

Hypothesis
orim1i.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \vee \chi \rightarrow \psi \vee \chi \)
Proof
l0
orim1i.1
id
orim12i l0 _