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