Theorem int-ineqmvtd

Description: IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

	Ref	Expression
Hypotheses	int-ineqmvtd.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	int-ineqmvtd.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	int-ineqmvtd.3	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
	int-ineqmvtd.4	⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
	int-ineqmvtd.5	⊢ ( 𝜑 → 𝐴 = ( 𝐶 + 𝐷 ) )
Assertion	int-ineqmvtd	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) ≤ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		int-ineqmvtd.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2		int-ineqmvtd.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3		int-ineqmvtd.3	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
4		int-ineqmvtd.4	⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
5		int-ineqmvtd.5	⊢ ( 𝜑 → 𝐴 = ( 𝐶 + 𝐷 ) )
6	4 5	breqtrd	⊢ ( 𝜑 → 𝐵 ≤ ( 𝐶 + 𝐷 ) )
7	1 3 2	lesubaddd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐷 ) ≤ 𝐶 ↔ 𝐵 ≤ ( 𝐶 + 𝐷 ) ) )
8	6 7	mpbird	⊢ ( 𝜑 → ( 𝐵 − 𝐷 ) ≤ 𝐶 )