Theorem le2addi

Description: Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999)

	Ref	Expression
Hypotheses	lt2.1	|- A e. RR
	lt2.2	|- B e. RR
	lt2.3	|- C e. RR
	lt.4	|- D e. RR
Assertion	le2addi	|- ( ( A <_ C /\ B <_ D ) -> ( A + B ) <_ ( C + D ) )

Proof

Step	Hyp	Ref	Expression
1		lt2.1	|- A e. RR
2		lt2.2	|- B e. RR
3		lt2.3	|- C e. RR
4		lt.4	|- D e. RR
5		le2add	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B <_ D ) -> ( A + B ) <_ ( C + D ) ) )
6	1 2 3 4 5	mp4an	|- ( ( A <_ C /\ B <_ D ) -> ( A + B ) <_ ( C + D ) )