Metamath Proof Explorer


Theorem sqvali

Description: Value of square. Inference version. (Contributed by NM, 1-Aug-1999)

Ref Expression
Hypothesis sqval.1 ⊢ A ∈ ℂ
Assertion sqvali ⊢ A 2 = A ⁢ A

Proof

Step Hyp Ref Expression
1 sqval.1 ⊢ A ∈ ℂ
2 sqval ⊢ A ∈ ℂ → A 2 = A ⁢ A
3 1 2 ax-mp ⊢ A 2 = A ⁢ A