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	⊢ ( ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → 𝜓 )
Assertion	jaoi2	⊢ ( ( 𝜑 ∨ 𝜒 ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		jaoi2.1	⊢ ( ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → 𝜓 )
2		pm5.63	⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜑 ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
3	2 1	sylbi	⊢ ( ( 𝜑 ∨ 𝜒 ) → 𝜓 )