Metamath Proof Explorer


Theorem int-mulassocd

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

Ref Expression
Hypotheses int-mulassocd.1
|- ( ph -> B e. RR )
int-mulassocd.2
|- ( ph -> C e. RR )
int-mulassocd.3
|- ( ph -> D e. RR )
int-mulassocd.4
|- ( ph -> A = B )
Assertion int-mulassocd
|- ( ph -> ( B x. ( C x. D ) ) = ( ( A x. C ) x. D ) )

Proof

Step Hyp Ref Expression
1 int-mulassocd.1
 |-  ( ph -> B e. RR )
2 int-mulassocd.2
 |-  ( ph -> C e. RR )
3 int-mulassocd.3
 |-  ( ph -> D e. RR )
4 int-mulassocd.4
 |-  ( ph -> A = B )
5 1 recnd
 |-  ( ph -> B e. CC )
6 2 recnd
 |-  ( ph -> C e. CC )
7 3 recnd
 |-  ( ph -> D e. CC )
8 5 6 7 mulassd
 |-  ( ph -> ( ( B x. C ) x. D ) = ( B x. ( C x. D ) ) )
9 4 eqcomd
 |-  ( ph -> B = A )
10 9 oveq1d
 |-  ( ph -> ( B x. C ) = ( A x. C ) )
11 10 oveq1d
 |-  ( ph -> ( ( B x. C ) x. D ) = ( ( A x. C ) x. D ) )
12 8 11 eqtr3d
 |-  ( ph -> ( B x. ( C x. D ) ) = ( ( A x. C ) x. D ) )