Theorem int-ineqmvtd

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

	Ref	Expression
Hypotheses	int-ineqmvtd.1	|- ( ph -> B e. RR )
	int-ineqmvtd.2	|- ( ph -> C e. RR )
	int-ineqmvtd.3	|- ( ph -> D e. RR )
	int-ineqmvtd.4	|- ( ph -> B <_ A )
	int-ineqmvtd.5	|- ( ph -> A = ( C + D ) )
Assertion	int-ineqmvtd	|- ( ph -> ( B - D ) <_ C )

Proof

Step	Hyp	Ref	Expression
1		int-ineqmvtd.1	|- ( ph -> B e. RR )
2		int-ineqmvtd.2	|- ( ph -> C e. RR )
3		int-ineqmvtd.3	|- ( ph -> D e. RR )
4		int-ineqmvtd.4	|- ( ph -> B <_ A )
5		int-ineqmvtd.5	|- ( ph -> A = ( C + D ) )
6	4 5	breqtrd	|- ( ph -> B <_ ( C + D ) )
7	1 3 2	lesubaddd	|- ( ph -> ( ( B - D ) <_ C <-> B <_ ( C + D ) ) )
8	6 7	mpbird	|- ( ph -> ( B - D ) <_ C )