Metamath Proof Explorer


Theorem divmulass

Description: An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021)

Ref Expression
Assertion divmulass ABCDD0ABDC=ABCD

Proof

Step Hyp Ref Expression
1 simpl1 ABCDD0A
2 simpl2 ABCDD0B
3 simpr ABCDD0DD0
4 divass ABDD0ABD=ABD
5 1 2 3 4 syl3anc ABCDD0ABD=ABD
6 5 eqcomd ABCDD0ABD=ABD
7 6 oveq1d ABCDD0ABDC=ABDC
8 mulcl ABAB
9 8 3adant3 ABCAB
10 9 adantr ABCDD0AB
11 simpl3 ABCDD0C
12 div32 ABDD0CABDC=ABCD
13 10 3 11 12 syl3anc ABCDD0ABDC=ABCD
14 7 13 eqtrd ABCDD0ABDC=ABCD