Metamath Proof Explorer


Theorem int-add02d

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

Ref Expression
Hypotheses int-add02d.1 ( 𝜑𝐴 ∈ ℝ )
int-add02d.2 ( 𝜑𝐴 = 𝐵 )
Assertion int-add02d ( 𝜑 → ( 0 + 𝐴 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 int-add02d.1 ( 𝜑𝐴 ∈ ℝ )
2 int-add02d.2 ( 𝜑𝐴 = 𝐵 )
3 1 recnd ( 𝜑𝐴 ∈ ℂ )
4 3 addid2d ( 𝜑 → ( 0 + 𝐴 ) = 𝐴 )
5 4 2 eqtrd ( 𝜑 → ( 0 + 𝐴 ) = 𝐵 )