Theorem orri

Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.)

Hypothesis
orri.1
\( \vdash \neg \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \vee \psi \)
Proof
l0
orri.1
\( \vdash \neg \varphi \rightarrow \psi \)
df-or
\( \vdash \varphi \vee \psi \leftrightarrow \neg \varphi \rightarrow \psi \)
mpbir l0 _