Metamath Proof Explorer


Theorem ltm1d

Description: A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypothesis ltp1d.1 φA
Assertion ltm1d φA1<A

Proof

Step Hyp Ref Expression
1 ltp1d.1 φA
2 ltm1 AA1<A
3 1 2 syl φA1<A