![]() |
Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > QLE Home > Th. List > ror | GIF version |
Description: Inference introducing disjunct to right. (Contributed by NM, 26-May-2008.) (Revised by NM, 31-Mar-2011.) |
Ref | Expression |
---|---|
lor.1 | a = b |
Ref | Expression |
---|---|
ror | (a ∪ c) = (b ∪ c) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lor.1 | . 2 a = b | |
2 | 1 | ax-r5 38 | 1 (a ∪ c) = (b ∪ c) |
Colors of variables: term |
Syntax hints: = wb 1 ∪ wo 6 |
This theorem was proved from axioms: ax-r5 38 |
This theorem is referenced by: k1-7 354 k1-8a 355 k1-8b 356 oa3moa3 1029 mli 1124 mlduali 1126 vneulem3 1131 vneulem6 1134 vneulem7 1135 vneulem9 1137 vneulem11 1139 vneulem12 1140 vneulemexp 1146 dp15lema 1152 dp15lemc 1154 dp15leme 1156 dp15lemf 1157 dp15lemg 1158 dp53lema 1161 dp53lemf 1166 dp35lem0 1177 dp41lemc0 1182 dp41lemf 1186 dp41lemg 1187 dp41lemk 1190 dp32 1194 xdp41 1196 xdp15 1197 xdp53 1198 xxdp41 1199 xxdp15 1200 xxdp53 1201 xdp45lem 1202 xdp43lem 1203 xdp45 1204 xdp43 1205 3dp43 1206 testmod 1211 testmod2 1213 testmod2expanded 1214 |
Copyright terms: Public domain | W3C validator |