3re - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 3re		Unicode version

Theorem 3re 9380

Description: The number 3 is real. (Contributed by NM, 27-May-1999.)

**Assertion**
Ref	Expression
3re

**Proof of Theorem 3re**
Step	Hyp	Ref	Expression
1		df-3 9366	. 2
2		2re 9376	. . 3
3		1re 8325	. . 3
4	2, 3	readdcli 8339	. 2
5	1, 4	eqeltri 2311	1

Colors of variables: wff set class

This proof depends on syntax axioms:

wcel 2209 (class class class)co 6085

cr 8178

c1 8180

caddc 8182

c2 9357

c3 9358

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1500 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-4 1563 ax-17 1579 ax-ial 1587 ax-ext 2220 ax-1re 8273 ax-addrcl 8276

This proof depends on definitions: df-bi 117 df-cleq 2231 df-clel 2234 df-2 9365 df-3 9366

This theorem is used by: 3cn 9381 4re 9383 3ne0 9401 3ap0 9402 4pos 9403 1lt3 9480 3lt4 9481 2lt4 9482 3lt5 9485 3lt6 9490 2lt6 9491 3lt7 9496 2lt7 9497 3lt8 9503 2lt8 9504 3lt9 9511 2lt9 9512 1le3 9520 8th4div3 9528 halfpm6th 9529 3halfnz 9747 3lt10 9922 2lt10 9923 5eluz3 9970 uzuzle23 9971 uzuzle34 9973 uz3m2nn 9982 nn01to3 10026 3rp 10070 fz0to4untppr 10541 expnass 11095 sqrt9 11828 ef01bndlem 12539 sin01bnd 12540 cos2bnd 12543 sin01gt0 12545 cos01gt0 12546 egt2lt3 12563 flodddiv4 12719 starvndxnmulrndx 13547 scandxnmulrndx 13559 vscandxnmulrndx 13564 ipndxnmulrndx 13577 tsetndxnmulrndx 13596 plendxnmulrndx 13610 dsndxnmulrndx 13625 slotsdifunifndx 13635 dveflem 15876 sincosq3sgn 15979 sincosq4sgn 15980 cosq23lt0 15984 coseq0q4123 15985 coseq00topi 15986 coseq0negpitopi 15987 tangtx 15989 sincos6thpi 15993 pigt3 15995 pige3 15996 cos02pilt1 16002 log2tlbndlog2 16139 log2ublog2 16143 ppiqub 16194 bposlem2 16210 bposlem3 16211 bposlem4 16212 bposlem5 16213 lgsdir2lem1 16245 2lgslem3 16318 konigsbergiedgwen 16823 konigsberglem1 16827 konigsberglem2 16828 konigsberglem3 16829 konigsberglem4 16830 ex-fl 16837 ex-gcd 16843