Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > bile | Unicode version |
Description: Biconditional to l.e. |
Ref | Expression |
---|---|
bile.1 |
Ref | Expression |
---|---|
bile |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bile.1 | . . . 4 | |
2 | 1 | ax-r5 38 | . . 3 |
3 | oridm 110 | . . 3 | |
4 | 2, 3 | ax-r2 36 | . 2 |
5 | 4 | df-le1 130 | 1 |
Colors of variables: term |
Syntax hints: wb 1 wle 2 wo 6 |
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: qlhoml1a 143 qlhoml1b 144 leid 148 str 189 mccune2 247 wom3 367 i3ri3 538 i3li3 539 i32i3 540 u12lem 771 sadm3 838 mlaconj4 844 mlaconjo 886 oaidlem2 931 oaidlem2g 932 distoah1 940 d3oa 995 oadist2 1009 mloa 1018 oadist 1019 dp15lemf 1157 dp35leme 1171 dp35lemd 1172 xdp15 1197 xxdp15 1200 xdp45lem 1202 xdp43lem 1203 xdp45 1204 xdp43 1205 3dp43 1206 |
Copyright terms: Public domain | W3C validator |