![]() |
Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > QLE Home > Th. List > ler2an | GIF version |
Description: Conjunction of 2 l.e.'s. (Contributed by NM, 11-Nov-1997.) |
Ref | Expression |
---|---|
ler2.1 | a ≤ b |
ler2.2 | a ≤ c |
Ref | Expression |
---|---|
ler2an | a ≤ (b ∩ c) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anidm 111 | . . 3 (a ∩ a) = a | |
2 | 1 | ax-r1 35 | . 2 a = (a ∩ a) |
3 | ler2.1 | . . 3 a ≤ b | |
4 | ler2.2 | . . 3 a ≤ c | |
5 | 3, 4 | le2an 169 | . 2 (a ∩ a) ≤ (b ∩ c) |
6 | 2, 5 | bltr 138 | 1 a ≤ (b ∩ c) |
Colors of variables: term |
Syntax hints: ≤ wle 2 ∩ 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 |
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: distlem 188 str 189 womao 220 womaon 221 womaa 222 womaan 223 anorabs2 224 mccune2 247 oaidlem1 294 nom14 311 id5leid0 351 k1-8a 355 2vwomlem 365 ska4 433 i3orlem7 558 ud3lem1a 566 ud4lem1b 578 ud5lem1b 587 bi1o1a 798 biao 799 i2i1i1 800 3vth2 805 3vth6 809 3vded21 817 oaeqv 830 mlaconj4 844 negantlem2 849 negantlem9 859 negantlem10 861 neg3antlem2 865 mhlem 876 mhlem2 878 mh 879 distid 887 oago3.21x 890 cancellem 891 govar2 897 gon2n 898 gomaex4 900 oas 925 oat 927 oau 929 oa23 936 oa4lem1 937 oa4lem2 938 oaliv 1003 oagen1 1014 oa3moa3 1029 4oaiii 1040 4oagen1 1042 lem3.3.3lem3 1051 lem3.3.7i4e1 1069 lem3.3.7i4e2 1070 lem3.3.7i5e1 1072 lem3.4.3 1076 com3iia 1100 lem4.6.7 1101 ml 1121 mldual2i 1125 ml3le 1127 vneulem1 1129 vneulem6 1134 vneulem7 1135 vneulem13 1141 vneulemexp 1146 dp53lema 1161 dp53lemc 1163 dp53lemd 1164 dp53lemf 1166 dp35lemd 1172 dp35lemc 1173 dp41lemh 1188 dp32 1194 xdp41 1196 xdp53 1198 xxdp41 1199 xxdp53 1201 xdp45lem 1202 xdp43lem 1203 xdp45 1204 xdp43 1205 3dp43 1206 oadp35lemc 1209 testmod2 1213 testmod2expanded 1214 |
Copyright terms: Public domain | W3C validator |