Metamath Proof Explorer


Theorem sn-addid0

Description: A number that sums to itself is zero. Compare addid0 , readdid1addid2d . (Contributed by SN, 5-May-2024)

Ref Expression
Hypotheses sn-addid0.a φ A
sn-addid0.1 φ A + A = A
Assertion sn-addid0 φ A = 0

Proof

Step Hyp Ref Expression
1 sn-addid0.a φ A
2 sn-addid0.1 φ A + A = A
3 sn-addid1 A A + 0 = A
4 1 3 syl φ A + 0 = A
5 2 4 eqtr4d φ A + A = A + 0
6 0cnd φ 0
7 1 1 6 sn-addcand φ A + A = A + 0 A = 0
8 5 7 mpbid φ A = 0