Description: An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | divmulass | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 | |
|
2 | simpl2 | |
|
3 | simpr | |
|
4 | divass | |
|
5 | 1 2 3 4 | syl3anc | |
6 | 5 | eqcomd | |
7 | 6 | oveq1d | |
8 | mulcl | |
|
9 | 8 | 3adant3 | |
10 | 9 | adantr | |
11 | simpl3 | |
|
12 | div32 | |
|
13 | 10 3 11 12 | syl3anc | |
14 | 7 13 | eqtrd | |