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

Theorem readdcld 6852
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 6805 . 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 6710   + caddc 6714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addrcl 6780
This theorem is referenced by:  ltadd2  7212  leadd1  7220  le2add  7234  lt2add  7235  lesub2  7247  ltsub2  7249  gt0add  7357  reapadd1  7380  apadd1  7392  mulext1  7396  recexaplem2  7415  recp1lt1  7646  cju  7694  peano5nni  7698  peano2nn  7707  peano2z  8057  expnbnd  9025  remim  9088  remullem  9099
  Copyright terms: Public domain W3C validator