Theorem olcd

Deduction introducing a disjunct. A translation of natural deduction rule \/ IL ( \/ insertion left), see [natded]. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis
orcd.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \vee \psi \)
Proof
orcd.1
orcd _
orcomd _