Theorem jaoi3

Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.)

Hypotheses
jaoi3.1
\( \vdash \varphi \rightarrow \psi \)
jaoi3.2
\( \vdash \neg \varphi \wedge \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \vee \chi \rightarrow \psi \)
Proof
l0
jaoi3.1
jaoi3.2
jaoi l0 _
jaoi2 _