Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  vneulem2 GIF version

Theorem vneulem2 1132
 Description: Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
Assertion
Ref Expression
vneulem2 (((xy) ∪ u) ∩ ((uw) ∩ w)) = ((((xy) ∩ (uw)) ∪ u) ∩ w)

Proof of Theorem vneulem2
StepHypRef Expression
1 anass 76 . . 3 ((((xy) ∪ u) ∩ (uw)) ∩ w) = (((xy) ∪ u) ∩ ((uw) ∩ w))
21cm 61 . 2 (((xy) ∪ u) ∩ ((uw) ∩ w)) = ((((xy) ∪ u) ∩ (uw)) ∩ w)
3 ax-a2 31 . . . . 5 ((xy) ∪ u) = (u ∪ (xy))
43ran 78 . . . 4 (((xy) ∪ u) ∩ (uw)) = ((u ∪ (xy)) ∩ (uw))
5 ml 1123 . . . . 5 (u ∪ ((xy) ∩ (uw))) = ((u ∪ (xy)) ∩ (uw))
65cm 61 . . . 4 ((u ∪ (xy)) ∩ (uw)) = (u ∪ ((xy) ∩ (uw)))
7 orcom 73 . . . 4 (u ∪ ((xy) ∩ (uw))) = (((xy) ∩ (uw)) ∪ u)
84, 6, 73tr 65 . . 3 (((xy) ∪ u) ∩ (uw)) = (((xy) ∩ (uw)) ∪ u)
98ran 78 . 2 ((((xy) ∪ u) ∩ (uw)) ∩ w) = ((((xy) ∩ (uw)) ∪ u) ∩ w)
102, 9tr 62 1 (((xy) ∪ u) ∩ ((uw) ∩ w)) = ((((xy) ∩ (uw)) ∪ u) ∩ w)
 Colors of variables: term Syntax hints:   = wb 1   ∪ wo 6   ∩ wa 7 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1122 This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131 This theorem is referenced by:  vneulem4  1134
 Copyright terms: Public domain W3C validator