Metamath Proof Explorer


Theorem xaddridd

Description: 0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis xaddridd.1 φ A *
Assertion xaddridd φ A + 𝑒 0 = A

Proof

Step Hyp Ref Expression
1 xaddridd.1 φ A *
2 xaddrid A * A + 𝑒 0 = A
3 1 2 syl φ A + 𝑒 0 = A