Metamath Proof Explorer


Theorem ltp1i

Description: A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001)

Ref Expression
Hypothesis ltplus1.1 A
Assertion ltp1i A<A+1

Proof

Step Hyp Ref Expression
1 ltplus1.1 A
2 ltp1 AA<A+1
3 1 2 ax-mp A<A+1