![]() |
Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > QLE Home > Th. List > vneulem15 | GIF version |
Description: Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.) |
Ref | Expression |
---|---|
vneulem13.1 | ((a ∪ b) ∩ (c ∪ d)) = 0 |
Ref | Expression |
---|---|
vneulem15 | ((a ∪ c) ∩ (b ∪ d)) = ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vneulem13.1 | . . . 4 ((a ∪ b) ∩ (c ∪ d)) = 0 | |
2 | 1 | vneulem10 1140 | . . 3 (((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) = (a ∪ c) |
3 | 1 | vneulem8 1138 | . . 3 (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d)) = (b ∪ d) |
4 | 2, 3 | 2an 79 | . 2 ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) = ((a ∪ c) ∩ (b ∪ d)) |
5 | 4 | cm 61 | 1 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∪ b) ∪ c) ∩ ((a ∪ c) ∪ d)) ∩ (((a ∪ b) ∪ d) ∩ ((b ∪ c) ∪ d))) |
Colors of variables: term |
Syntax hints: = wb 1 ∪ wo 6 ∩ wa 7 0wf 9 |
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: vneulem 1147 |
Copyright terms: Public domain | W3C validator |