Metamath Proof Explorer


Theorem 3cn

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022)

Ref Expression
Assertion 3cn 3

Proof

Step Hyp Ref Expression
1 df-3 3 = 2 + 1
2 2cn 2
3 ax-1cn 1
4 2 3 addcli 2 + 1
5 1 4 eqeltri 3