| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > rexri | Unicode version | ||
| Description: A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
| Ref | Expression |
|---|---|
| rexri.1 |
|
| Ref | Expression |
|---|---|
| rexri |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rexri.1 |
. 2
| |
| 2 | rexr 8118 |
. 2
| |
| 3 | 1, 2 | ax-mp 5 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-v 2774 df-un 3170 df-in 3172 df-ss 3179 df-xr 8111 |
| This theorem is referenced by: 1xr 8131 cos12dec 12079 halfleoddlt 12205 reeff1oleme 15244 reeff1o 15245 sin0pilem2 15254 neghalfpirx 15266 sincosq1sgn 15298 sincosq2sgn 15299 sincosq4sgn 15301 sinq12gt0 15302 cosq14gt0 15304 cosq23lt0 15305 coseq0q4123 15306 coseq00topi 15307 coseq0negpitopi 15308 cosordlem 15321 cosq34lt1 15322 cos02pilt1 15323 cos0pilt1 15324 ioocosf1o 15326 negpitopissre 15327 iooref1o 15973 taupi 16012 |
| Copyright terms: Public domain | W3C validator |