Metamath Proof Explorer

Theorem wl-orel12

Description: In a conjunctive normal form a pair of nodes like ( ph \/ ps ) /\ ( -. ph \/ ch ) eliminates the need of a node ( ps \/ ch ) . This theorem allows simplifications in that respect. (Contributed by Wolf Lammen, 20-Jun-2020)

Ref Expression
Assertion wl-orel12 ⊢ φ ∨ ψ ∧ ¬ φ ∨ χ → ψ ∨ χ

Proof

Step Hyp Ref Expression
1 pm2.1 ⊢ ¬ φ ∨ φ
2 orel1 ⊢ ¬ φ → φ ∨ ψ → ψ
3 orc ⊢ ψ → ψ ∨ χ
4 2 3 syl6com ⊢ φ ∨ ψ → ¬ φ → ψ ∨ χ
5 notnot ⊢ φ → ¬ ¬ φ
6 orel1 ⊢ ¬ ¬ φ → ¬ φ ∨ χ → χ
7 5 6 syl ⊢ φ → ¬ φ ∨ χ → χ
8 olc ⊢ χ → ψ ∨ χ
9 7 8 syl6com ⊢ ¬ φ ∨ χ → φ → ψ ∨ χ
10 4 9 jaao ⊢ φ ∨ ψ ∧ ¬ φ ∨ χ → ¬ φ ∨ φ → ψ ∨ χ
11 1 10 mpi ⊢ φ ∨ ψ ∧ ¬ φ ∨ χ → ψ ∨ χ