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 AA+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+0A=0
8 5 7 mpbid φA=0