Metamath Proof Explorer


Theorem int-mulassocd

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

Ref Expression
Hypotheses int-mulassocd.1 φB
int-mulassocd.2 φC
int-mulassocd.3 φD
int-mulassocd.4 φA=B
Assertion int-mulassocd φBCD=ACD

Proof

Step Hyp Ref Expression
1 int-mulassocd.1 φB
2 int-mulassocd.2 φC
3 int-mulassocd.3 φD
4 int-mulassocd.4 φA=B
5 1 recnd φB
6 2 recnd φC
7 3 recnd φD
8 5 6 7 mulassd φBCD=BCD
9 4 eqcomd φB=A
10 9 oveq1d φBC=AC
11 10 oveq1d φBCD=ACD
12 8 11 eqtr3d φBCD=ACD