Metamath Proof Explorer


Theorem nn0sub2

Description: Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005)

Ref Expression
Assertion nn0sub2 M0N0MNNM0

Proof

Step Hyp Ref Expression
1 nn0sub M0N0MNNM0
2 1 biimp3a M0N0MNNM0