Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > leror | GIF version |
Description: Add disjunct to right of both sides. |
Ref | Expression |
---|---|
le.1 | a ≤ b |
Ref | Expression |
---|---|
leror | (a ∪ c) ≤ (b ∪ c) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orordir 113 | . . . 4 ((a ∪ b) ∪ c) = ((a ∪ c) ∪ (b ∪ c)) | |
2 | 1 | ax-r1 35 | . . 3 ((a ∪ c) ∪ (b ∪ c)) = ((a ∪ b) ∪ c) |
3 | le.1 | . . . . 5 a ≤ b | |
4 | 3 | df-le2 131 | . . . 4 (a ∪ b) = b |
5 | 4 | ax-r5 38 | . . 3 ((a ∪ b) ∪ c) = (b ∪ c) |
6 | 2, 5 | ax-r2 36 | . 2 ((a ∪ c) ∪ (b ∪ c)) = (b ∪ c) |
7 | 6 | df-le1 130 | 1 (a ∪ c) ≤ (b ∪ c) |
Colors of variables: term |
Syntax hints: ≤ wle 2 ∪ wo 6 |
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 |
This theorem depends on definitions: df-t 41 df-f 42 df-le1 130 df-le2 131 |
This theorem is referenced by: lelor 166 le2or 168 ka4lemo 228 ska13 241 wql2lem 288 womle2a 295 nom24 317 i5lei1 347 i5lei2 348 i5lei3 349 ska2 432 ska4 433 ka4ot 435 cmtr1com 493 ud4lem3a 583 ud4lem3b 584 comi1 709 3vded21 817 3vded22 818 3vroa 831 sa5 836 negantlem2 849 negantlem3 850 negantlem9 859 elimconslem 867 elimcons 868 comanb 872 e2ast2 894 oa4uto4g 975 oagen1 1014 4oagen1 1042 lem3.3.3lem1 1049 lem3.3.3lem2 1050 vneulem6 1134 vneulemexp 1146 l42modlem2 1148 dp15lema 1152 dp15lemf 1157 dp53leme 1165 dp41lemb 1181 dp41leme 1185 dp23 1195 xdp41 1196 xdp15 1197 xdp53 1198 xxdp41 1199 xxdp15 1200 xxdp53 1201 xdp45lem 1202 xdp43lem 1203 xdp45 1204 xdp43 1205 3dp43 1206 testmod2 1213 testmod2expanded 1214 |
Copyright terms: Public domain | W3C validator |