Theorem olci

Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)

Hypothesis
orci.1
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \vee \varphi \)
Proof
orci.1
a1i _
orri _