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

Theorem wl-cases2-dnf 31757
 Description: A particular instance of orddi 877 and anddi 878 converting between disjunctive and conjunctive normal forms, when both and appear. This theorem in fact rephrases cases2 980, and is related to consensus 967. I restate it here in DNF and CNF. The proof deliberately does not use df-ifp 1421 and dfifp4 1424, 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
StepHypRef Expression
1 exmid 416 . . . . 5
21biantrur 508 . . . 4
3 orcom 388 . . . . 5
4 orcom 388 . . . . 5
53, 4anbi12i 701 . . . 4
62, 5anbi12i 701 . . 3
7 anass 653 . . 3
8 orddi 877 . . 3
96, 7, 83bitr4ri 281 . 2
10 wl-orel12 31756 . . 3
1110pm4.71i 636 . 2
12 ancom 451 . 2
139, 11, 123bitr2i 276 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 187   wo 369   wa 370 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 188  df-or 371  df-an 372 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator