Metamath Proof Explorer


Theorem sqmul

Description: Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008)

Ref Expression
Assertion sqmul ABAB2=A2B2

Proof

Step Hyp Ref Expression
1 2nn0 20
2 mulexp AB20AB2=A2B2
3 1 2 mp3an3 ABAB2=A2B2