Metamath Proof Explorer


Theorem cnre

Description: Alias for ax-cnre , for naming consistency. (Contributed by NM, 3-Jan-2013)

Ref Expression
Assertion cnre A x y A = x + i y

Proof

Step Hyp Ref Expression
1 ax-cnre A x y A = x + i y