Metamath Proof Explorer


Theorem imaddi

Description: Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999)

Ref Expression
Hypotheses recl.1 A
readdi.2 B
Assertion imaddi A+B=A+B

Proof

Step Hyp Ref Expression
1 recl.1 A
2 readdi.2 B
3 imadd ABA+B=A+B
4 1 2 3 mp2an A+B=A+B