Theorem jaoi2

Description: 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)

	Ref	Expression
Hypothesis	jaoi2.1	$$⊢\left(\phi \vee \left(\neg \phi \wedge \chi \right)\right)\to \psi$$
Assertion	jaoi2	$$⊢\left(\phi \vee \chi \right)\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		jaoi2.1	$$⊢\left(\phi \vee \left(\neg \phi \wedge \chi \right)\right)\to \psi$$
2		pm5.63	$$⊢\left(\phi \vee \chi \right)\leftrightarrow \left(\phi \vee \left(\neg \phi \wedge \chi \right)\right)$$
3	2 1	sylbi	$$⊢\left(\phi \vee \chi \right)\to \psi$$