Theorem
orim2i
Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
Hypothesis
orim1i.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \chi \vee \varphi \rightarrow \chi \vee \psi \)
Proof
l0
id
orim1i.1
orim12i
l0
_
This is the content in the right pane.