Metamath Proof Explorer

Theorem sqvali

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

Ref Expression
Hypothesis sqval.1 
|- A e. CC
Assertion sqvali 
|- ( A ^ 2 ) = ( A x. A )

Proof

Step Hyp Ref Expression
1 sqval.1 
 |-  A e. CC
2 sqval 
 |-  ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
3 1 2 ax-mp 
 |-  ( A ^ 2 ) = ( A x. A )