Metamath Proof Explorer

Theorem wl-cases2-dnf

Description: A particular instance of orddi and anddi converting between disjunctive and conjunctive normal forms, when both ph and -. ph appear. This theorem in fact rephrases cases2 , and is related to consensus . I restate it here in DNF and CNF. The proof deliberately does not use df-ifp and dfifp4 , by which it can be shortened. (Contributed by Wolf Lammen, 21-Jun-2020) (Proof modification is discouraged.)

Ref Expression
Assertion wl-cases2-dnf ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ

Proof

Step Hyp Ref Expression
1 exmid ⊢ φ ∨ ¬ φ
2 1 biantrur ⊢ φ ∨ χ ↔ φ ∨ ¬ φ ∧ φ ∨ χ
3 orcom ⊢ ¬ φ ∨ ψ ↔ ψ ∨ ¬ φ
4 orcom ⊢ χ ∨ ψ ↔ ψ ∨ χ
5 3 4 anbi12i ⊢ ¬ φ ∨ ψ ∧ χ ∨ ψ ↔ ψ ∨ ¬ φ ∧ ψ ∨ χ
6 2 5 anbi12i ⊢ φ ∨ χ ∧ ¬ φ ∨ ψ ∧ χ ∨ ψ ↔ φ ∨ ¬ φ ∧ φ ∨ χ ∧ ψ ∨ ¬ φ ∧ ψ ∨ χ
7 anass ⊢ φ ∨ χ ∧ ¬ φ ∨ ψ ∧ χ ∨ ψ ↔ φ ∨ χ ∧ ¬ φ ∨ ψ ∧ χ ∨ ψ
8 orddi ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ φ ∨ ¬ φ ∧ φ ∨ χ ∧ ψ ∨ ¬ φ ∧ ψ ∨ χ
9 6 7 8 3bitr4ri ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ φ ∨ χ ∧ ¬ φ ∨ ψ ∧ χ ∨ ψ
10 wl-orel12 ⊢ φ ∨ χ ∧ ¬ φ ∨ ψ → χ ∨ ψ
11 10 pm4.71i ⊢ φ ∨ χ ∧ ¬ φ ∨ ψ ↔ φ ∨ χ ∧ ¬ φ ∨ ψ ∧ χ ∨ ψ
12 ancom ⊢ φ ∨ χ ∧ ¬ φ ∨ ψ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ
13 9 11 12 3bitr2i ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ