Metamath Proof Explorer

Theorem nna0

Description: Addition with zero. Theorem 4I(A1) of Enderton p. 79. (Contributed by NM, 20-Sep-1995)

Ref Expression
Assertion nna0 A ω A + 𝑜 = A


Step Hyp Ref Expression
1 nnon A ω A On
2 oa0 A On A + 𝑜 = A
3 1 2 syl A ω A + 𝑜 = A