Metamath Proof Explorer


Theorem leaddsuble

Description: Addition and subtraction on one side of "less than or equal to". (Contributed by Alexander van der Vekens, 18-Mar-2018)

Ref Expression
Assertion leaddsuble A B C B C A + B - C A

Proof

Step Hyp Ref Expression
1 leadd2 B C A B C A + B A + C
2 1 3comr A B C B C A + B A + C
3 readdcl A B A + B
4 3 3adant3 A B C A + B
5 simp3 A B C C
6 simp1 A B C A
7 4 5 6 lesubaddd A B C A + B - C A A + B A + C
8 2 7 bitr4d A B C B C A + B - C A