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

Theorem readdcld 6812
Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1 (φA ℝ)
readdcld.2 (φB ℝ)
Assertion
Ref Expression
readdcld (φ → (A + B) ℝ)

Proof of Theorem readdcld
StepHypRef Expression
1 recnd.1 . 2 (φA ℝ)
2 readdcld.2 . 2 (φB ℝ)
3 readdcl 6765 . 2 ((A B ℝ) → (A + B) ℝ)
41, 2, 3syl2anc 391 1 (φ → (A + B) ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  (class class class)co 5455  cr 6670   + caddc 6674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addrcl 6740
This theorem is referenced by:  ltadd2  7172  leadd1  7180  le2add  7194  lt2add  7195  lesub2  7207  ltsub2  7209  gt0add  7317  reapadd1  7340  apadd1  7352  mulext1  7356  recexaplem2  7375  recp1lt1  7606  cju  7654  peano5nni  7658  peano2nn  7667  peano2z  8017  expnbnd  8985  remim  9048  remullem  9059
  Copyright terms: Public domain W3C validator