Theorem xle2addd

Description: Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	xle2addd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
	xle2addd.2	$$⊢\phi \to B\in {ℝ}^{*}$$
	xle2addd.3	$$⊢\phi \to C\in {ℝ}^{*}$$
	xle2addd.4	$$⊢\phi \to D\in {ℝ}^{*}$$
	xle2addd.5	$$⊢\phi \to A\le C$$
	xrle2addd.6	$$⊢\phi \to B\le D$$
Assertion	xle2addd	$$⊢\phi \to A{+}_{𝑒}B\le C{+}_{𝑒}D$$

Proof

Step	Hyp	Ref	Expression
1		xle2addd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xle2addd.2	$$⊢\phi \to B\in {ℝ}^{*}$$
3		xle2addd.3	$$⊢\phi \to C\in {ℝ}^{*}$$
4		xle2addd.4	$$⊢\phi \to D\in {ℝ}^{*}$$
5		xle2addd.5	$$⊢\phi \to A\le C$$
6		xrle2addd.6	$$⊢\phi \to B\le D$$
7	1 2	xaddcld	$$⊢\phi \to A{+}_{𝑒}B\in {ℝ}^{*}$$
8	1 4	xaddcld	$$⊢\phi \to A{+}_{𝑒}D\in {ℝ}^{*}$$
9	3 4	xaddcld	$$⊢\phi \to C{+}_{𝑒}D\in {ℝ}^{*}$$
10	2 4 1 6	xleadd2d	$$⊢\phi \to A{+}_{𝑒}B\le A{+}_{𝑒}D$$
11	1 3 4 5	xleadd1d	$$⊢\phi \to A{+}_{𝑒}D\le C{+}_{𝑒}D$$
12	7 8 9 10 11	xrletrd	$$⊢\phi \to A{+}_{𝑒}B\le C{+}_{𝑒}D$$