Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Stanislas Polu
INT Inequalities Proof Generator
int-mulassocd
Next ⟩
int-mulsimpd
Metamath Proof Explorer
Ascii
Unicode
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
⊢
φ
→
B
⁢
C
⁢
D
=
A
⁢
C
⁢
D
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
⊢
φ
→
B
⁢
C
⁢
D
=
B
⁢
C
⁢
D
9
4
eqcomd
⊢
φ
→
B
=
A
10
9
oveq1d
⊢
φ
→
B
⁢
C
=
A
⁢
C
11
10
oveq1d
⊢
φ
→
B
⁢
C
⁢
D
=
A
⁢
C
⁢
D
12
8
11
eqtr3d
⊢
φ
→
B
⁢
C
⁢
D
=
A
⁢
C
⁢
D