Theorem jao1i

Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)

Hypothesis
jao1i.1
\( \vdash \psi \rightarrow \chi \rightarrow \varphi \)
Conclusion
\( \vdash \varphi \vee \psi \rightarrow \chi \rightarrow \varphi \)
Proof
l0
ax-1
jao1i.1
jaoi l0 _