Metamath Proof Explorer


Theorem nn0ge0d

Description: A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis nn0red.1 φ A 0
Assertion nn0ge0d φ 0 A

Proof

Step Hyp Ref Expression
1 nn0red.1 φ A 0
2 nn0ge0 A 0 0 A
3 1 2 syl φ 0 A