![]() |
Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > QLE Home > Th. List > le2an | GIF version |
Description: Conjunction of 2 l.e.'s. |
Ref | Expression |
---|---|
le2.1 | a ≤ b |
le2.2 | c ≤ d |
Ref | Expression |
---|---|
le2an | (a ∩ c) ≤ (b ∩ d) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | le2.1 | . . 3 a ≤ b | |
2 | 1 | leran 153 | . 2 (a ∩ c) ≤ (b ∩ c) |
3 | le2.2 | . . 3 c ≤ d | |
4 | 3 | lelan 167 | . 2 (b ∩ c) ≤ (b ∩ d) |
5 | 2, 4 | letr 137 | 1 (a ∩ c) ≤ (b ∩ d) |
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: lel2an 171 ler2an 173 ledi 174 ledio 176 ska4 433 i3orlem2 553 i3orlem3 554 ud4lem1a 577 test2 803 mlaoml 833 orbile 843 mlaconj4 844 mhlem 876 mh 879 mlaconjo 886 oago3.21x 890 e2ast2 894 gon2n 898 go2n4 899 go2n6 901 oa4lem3 939 oa3to4lem3 947 oa4to6lem4 963 oa4btoc 966 oa4uto4g 975 oa4uto4 977 oa3-6lem 980 mloa 1018 l42modlem2 1148 dp53lemc 1163 dp35leme 1171 dp35lemc 1173 dp41lemb 1181 xdp41 1196 xdp53 1198 xxdp41 1199 xxdp53 1201 xdp45lem 1202 xdp43lem 1203 xdp45 1204 xdp43 1205 3dp43 1206 oadp35lemc 1209 |
Copyright terms: Public domain | W3C validator |