Theorem addgt0ii

Description: Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999)

	Ref	Expression
Hypotheses	lt2.1	$$⊢A\in ℝ$$
	lt2.2	$$⊢B\in ℝ$$
	addgt0i.3	$$⊢0<A$$
	addgt0i.4	$$⊢0<B$$
Assertion	addgt0ii	$$⊢0<A+B$$

Proof

Step	Hyp	Ref	Expression
1		lt2.1	$$⊢A\in ℝ$$
2		lt2.2	$$⊢B\in ℝ$$
3		addgt0i.3	$$⊢0<A$$
4		addgt0i.4	$$⊢0<B$$
5	1 2	addgt0i	$$⊢\left(0<A\wedge 0<B\right)\to 0<A+B$$
6	3 4 5	mp2an	$$⊢0<A+B$$