Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > orass | GIF version |
Description: Associative law. (Contributed by NM, 27-May-2008.) (Revised by NM, 31-Mar-2011.) |
Ref | Expression |
---|---|
orass | ((a ∪ b) ∪ c) = (a ∪ (b ∪ c)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-a3 32 | 1 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c)) |
Colors of variables: term |
Syntax hints: = wb 1 ∪ wo 6 |
This theorem was proved from axioms: ax-a3 32 |
This theorem is referenced by: oa3moa3 1029 vneulem12 1142 vneulemexp 1148 l42modlem1 1149 dp15lema 1154 dp15lemd 1157 dp15leme 1158 dp15lemg 1160 dp53leme 1167 dp35lemd 1174 dp34 1181 dp41lemc0 1184 dp41lemj 1191 xdp41 1198 xdp15 1199 xdp53 1200 xxdp41 1201 xxdp15 1202 xxdp53 1203 xdp45lem 1204 xdp43lem 1205 xdp45 1206 xdp43 1207 3dp43 1208 testmod 1213 testmod2 1215 testmod2expanded 1216 |
Copyright terms: Public domain | W3C validator |