ax-plus-zero - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-plus-zero

Axiom ax-plus-zero 496

Description: Addition with zero. A standard axiom of second-order arithmetic. Robinson's fourth axiom.

**Assertion**
Ref	Expression
ax-plus-zero	⊢ li + ku'i'a 0 du li ku'i'a

This axiom is referenced by: 1p0e1 498 sumji-no 501