Theorem orcd

Deduction introducing a disjunct. A translation of natural deduction rule \/ IR ( \/ insertion right), see [natded]. (Contributed by NM, 20-Sep-2007.)

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