Metamath Proof Explorer


Theorem xaddid1d

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

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

Proof

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