Metamath Proof Explorer


Theorem int-add01d

Description: First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

Ref Expression
Hypotheses int-add01d.1
|- ( ph -> A e. RR )
int-add01d.2
|- ( ph -> A = B )
Assertion int-add01d
|- ( ph -> ( A + 0 ) = B )

Proof

Step Hyp Ref Expression
1 int-add01d.1
 |-  ( ph -> A e. RR )
2 int-add01d.2
 |-  ( ph -> A = B )
3 1 recnd
 |-  ( ph -> A e. CC )
4 3 addid1d
 |-  ( ph -> ( A + 0 ) = A )
5 4 2 eqtrd
 |-  ( ph -> ( A + 0 ) = B )