Metamath Proof Explorer


Theorem ltadd2dd

Description: Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses ltd.1 φA
ltd.2 φB
letrd.3 φC
ltletrd.4 φA<B
Assertion ltadd2dd φC+A<C+B

Proof

Step Hyp Ref Expression
1 ltd.1 φA
2 ltd.2 φB
3 letrd.3 φC
4 ltletrd.4 φA<B
5 1 2 3 ltadd2d φA<BC+A<C+B
6 4 5 mpbid φC+A<C+B