Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > readdcli | Structured version Visualization version Unicode version |
Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Ref | Expression |
---|---|
recni.1 | |
axri.2 |
Ref | Expression |
---|---|
readdcli |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recni.1 | . 2 | |
2 | axri.2 | . 2 | |
3 | readdcl 10019 | . 2 | |
4 | 1, 2, 3 | mp2an 708 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 (class class class)co 6650 cr 9935 caddc 9939 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-addrcl 9997 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: resubcli 10343 eqneg 10745 ledivp1i 10949 ltdivp1i 10950 2re 11090 3re 11094 4re 11097 5re 11099 6re 11101 7re 11103 8re 11105 9re 11107 10reOLD 11109 numltc 11528 nn0opthlem2 13056 hashunlei 13212 hashge2el2dif 13262 abs3lemi 14149 ef01bndlem 14914 divalglem6 15121 log2ub 24676 mumullem2 24906 bposlem8 25016 dchrvmasumlem2 25187 ex-fl 27304 norm-ii-i 27994 norm3lem 28006 nmoptrii 28953 bdophsi 28955 unierri 28963 staddi 29105 stadd3i 29107 dp2ltc 29594 dpmul4 29622 ballotlem2 30550 hgt750lem 30729 poimirlem16 33425 itg2addnclem3 33463 fdc 33541 pellqrex 37443 stirlinglem11 40301 fouriersw 40448 zm1nn 41316 evengpoap3 41687 |
Copyright terms: Public domain | W3C validator |