wl-cases2-dnf - Mathbox for Wolf Lammen

	Mathbox for Wolf Lammen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-cases2-dnf		Structured version Visualization version Unicode version

Theorem wl-cases2-dnf 33295

Description: A particular instance of orddi 913 and anddi 914 converting between disjunctive and conjunctive normal forms, when both

and

appear. This theorem in fact rephrases cases2 993, and is related to consensus 999. I restate it here in DNF and CNF. The proof deliberately does not use df-ifp 1013 and dfifp4 1016, by which it can be shortened. (Contributed by Wolf Lammen, 21-Jun-2020.) (Proof modification is discouraged.)

**Assertion**
Ref	Expression
wl-cases2-dnf	$/\$ $\/$ $/\$ $\/$ $/\$ $\/$

**Proof of Theorem wl-cases2-dnf**
Step	Hyp	Ref	Expression
1		exmid 431	. . . . 5 $\/$
2	1	biantrur 527	. . . 4 $\/$ $\/$ $/\$ $\/$
3		orcom 402	. . . . 5 $\/$ $\/$
4		orcom 402	. . . . 5 $\/$ $\/$
5	3, 4	anbi12i 733	. . . 4 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
6	2, 5	anbi12i 733	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
7		anass 681	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
8		orddi 913	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
9	6, 7, 8	3bitr4ri 293	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
10		wl-orel12 33294	. . 3 $\/$ $/\$ $\/$ $\/$
11	10	pm4.71i 664	. 2 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
12		ancom 466	. 2 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
13	9, 11, 12	3bitr2i 288	1 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 196 $\/$ wo 383 $/\$ wa 384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386

This theorem is referenced by: (None)

W3C validator