Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > leid | GIF version |
Description: Identity law for less-than-or-equal. |
Ref | Expression |
---|---|
leid | a ≤ a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 59 | . 2 a = a | |
2 | 1 | bile 142 | 1 a ≤ a |
Colors of variables: term |
Syntax hints: ≤ wle 2 |
This theorem was proved from axioms: ax-a1 30 ax-a2 31 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 |
This theorem is referenced by: bi1o1a 798 i2i1i1 800 1oa 820 negantlem2 849 mhlem 876 oago3.21x 890 gomaex3h6 907 gomaex3h9 910 gomaex3lem2 915 oaur 930 oa4btoc 966 oa3-u2lem 986 oa3-6to3 987 oa3-2to4 988 oa3-u1 991 oa3-1to5 993 d3oa 995 d4oa 996 lem3.3.7i4e1 1069 lem3.3.7i4e2 1070 lem3.3.7i5e1 1072 lem4.6.6i0j1 1086 lem4.6.6i0j2 1087 lem4.6.6i0j3 1088 lem4.6.6i0j4 1089 lem4.6.6i2j4 1095 lem4.6.6i3j0 1096 lem4.6.6i3j1 1097 lem4.6.6i4j2 1099 com3iia 1100 lem4.6.7 1101 mldual2i 1125 vneulem1 1129 vneulem13 1141 vneulemexp 1146 dp53lema 1161 dp35lem0 1177 xdp53 1198 xxdp53 1201 xdp43lem 1203 xdp43 1205 3dp43 1206 |
Copyright terms: Public domain | W3C validator |