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