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	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		exmid	|- ( ph \/ -. ph )
2	1	biantrur	|- ( ( ph \/ ch ) <-> ( ( ph \/ -. ph ) /\ ( ph \/ ch ) ) )
3		orcom	|- ( ( -. ph \/ ps ) <-> ( ps \/ -. ph ) )
4		orcom	|- ( ( ch \/ ps ) <-> ( ps \/ ch ) )
5	3 4	anbi12i	|- ( ( ( -. ph \/ ps ) /\ ( ch \/ ps ) ) <-> ( ( ps \/ -. ph ) /\ ( ps \/ ch ) ) )
6	2 5	anbi12i	|- ( ( ( ph \/ ch ) /\ ( ( -. ph \/ ps ) /\ ( ch \/ ps ) ) ) <-> ( ( ( ph \/ -. ph ) /\ ( ph \/ ch ) ) /\ ( ( ps \/ -. ph ) /\ ( ps \/ ch ) ) ) )
7		anass	|- ( ( ( ( ph \/ ch ) /\ ( -. ph \/ ps ) ) /\ ( ch \/ ps ) ) <-> ( ( ph \/ ch ) /\ ( ( -. ph \/ ps ) /\ ( ch \/ ps ) ) ) )
8		orddi	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ( ph \/ -. ph ) /\ ( ph \/ ch ) ) /\ ( ( ps \/ -. ph ) /\ ( ps \/ ch ) ) ) )
9	6 7 8	3bitr4ri	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( ( ph \/ ch ) /\ ( -. ph \/ ps ) ) /\ ( ch \/ ps ) ) )
10		wl-orel12	|- ( ( ( ph \/ ch ) /\ ( -. ph \/ ps ) ) -> ( ch \/ ps ) )
11	10	pm4.71i	|- ( ( ( ph \/ ch ) /\ ( -. ph \/ ps ) ) <-> ( ( ( ph \/ ch ) /\ ( -. ph \/ ps ) ) /\ ( ch \/ ps ) ) )
12		ancom	|- ( ( ( ph \/ ch ) /\ ( -. ph \/ ps ) ) <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) )
13	9 11 12	3bitr2i	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) )