Metamath Proof Explorer


Theorem int-sqdefd

Description: SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

Ref Expression
Hypotheses int-sqdefd.1 φB
int-sqdefd.2 φA=B
Assertion int-sqdefd φAB=A2

Proof

Step Hyp Ref Expression
1 int-sqdefd.1 φB
2 int-sqdefd.2 φA=B
3 2 oveq1d φA2=B2
4 1 recnd φB
5 4 sqvald φB2=BB
6 eqcom A=BB=A
7 6 imbi2i φA=BφB=A
8 2 7 mpbi φB=A
9 8 oveq1d φBB=AB
10 5 9 eqtrd φB2=AB
11 3 10 eqtrd φA2=AB
12 11 eqcomd φAB=A2