Theorem readdcli 8345

Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	|- A e. RR
axri.2	|- B e. RR

Assertion

Ref	Expression
readdcli	|- ( A + B ) e. RR

Proof of Theorem readdcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 |- A e. RR
2		axri.2	. 2 |- B e. RR
3		readdcl 8311	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4	1, 2, 3	mp2an 430	1 |- ( A + B ) e. RR

This proof depends on syntax axioms:   e. wcel 2209  (class class class)co 6088   RRcr 8184   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addrcl 8282

This theorem is used by:  resubcli  8596  eqneg  9070  2re  9383  3re  9387  4re  9390  5re  9392  6re  9394  7re  9396  8re  9398  9re  9400  numltc  9818  ef01bndlem  12548  ballotfilem2  13286  log2ublog2  16224  bposlem8  16318  ex-fl  16944