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

Theorem readdcld 6944
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 6897 . 2 ((A B ℝ) → (A + B) ℝ)
41, 2, 3syl2anc 391 1 (φ → (A + B) ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1393  (class class class)co 5458  cr 6778   + caddc 6782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addrcl 6871
This theorem is referenced by:  ltadd2  7304  leadd1  7312  le2add  7326  lt2add  7327  lesub2  7339  ltsub2  7341  gt0add  7449  reapadd1  7472  apadd1  7484  mulext1  7488  recexaplem2  7507  recp1lt1  7738  cju  7786  peano5nni  7790  peano2nn  7799  peano2z  8149  expnbnd  9118  remim  9181  remullem  9192  caucvgrelemcau  9299  caucvgre  9300
  Copyright terms: Public domain W3C validator