Home
Metamath Proof Explorer
< Previous
Next >
Related theorems
GIF version
Syntax Definition
cpli
3767
Description:
Positive integer addition.
Assertion
Ref
Expression
cpli
class
+
N
See definition
df-pli
3795
for more information.
Colors of variables:
wff
set
class
metamath.org