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 ⊢φ∧ψ∨¬φ∧χ↔¬φ∨ψ∧φ∨χ