Theorem jaoi2

Inference removing a negated conjunct in a disjunction of an antecedent if this conjunct is part of the disjunction. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)

Hypothesis
jaoi2.1
\( \vdash \varphi \vee \neg \varphi \wedge \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \vee \chi \rightarrow \psi \)
Proof
l0
pm5.63
\( \vdash \varphi \vee \chi \leftrightarrow \varphi \vee \neg \varphi \wedge \chi \)
jaoi2.1
\( \vdash \varphi \vee \neg \varphi \wedge \chi \rightarrow \psi \)
sylbi l0 _