Metamath Proof Explorer


Theorem addid1d

Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis muld.1 φ A
Assertion addid1d φ A + 0 = A

Proof

Step Hyp Ref Expression
1 muld.1 φ A
2 addid1 A A + 0 = A
3 1 2 syl φ A + 0 = A