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

Theorem 3re 7989
Description: The number 3 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
3re 3 ∈ ℝ

Proof of Theorem 3re
StepHypRef Expression
1 df-3 7974 . 2 3 = (2 + 1)
2 2re 7985 . . 3 2 ∈ ℝ
3 1re 7026 . . 3 1 ∈ ℝ
42, 3readdcli 7040 . 2 (2 + 1) ∈ ℝ
51, 4eqeltri 2110 1 3 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1393  (class class class)co 5512  cr 6888  1c1 6890   + caddc 6892  2c2 7964  3c3 7965
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-1re 6978  ax-addrcl 6981
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-2 7973  df-3 7974
This theorem is referenced by:  3cn  7990  4re  7992  3ne0  8011  3ap0  8012  4pos  8013  1lt3  8088  3lt4  8089  2lt4  8090  3lt5  8093  3lt6  8098  2lt6  8099  3lt7  8104  2lt7  8105  3lt8  8111  2lt8  8112  3lt9  8119  2lt9  8120  3lt10  8128  2lt10  8129  1le3  8136  8th4div3  8144  halfpm6th  8145  uzuzle23  8513  uz3m2nn  8515  nn01to3  8552  expnass  9357  sqrt9  9646  ex-fl  9895
  Copyright terms: Public domain W3C validator