Metamath Proof Explorer


Theorem divmulasscom

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

Ref Expression
Assertion divmulasscom ABCDD0ABDC=BACD

Proof

Step Hyp Ref Expression
1 divmulass ABCDD0ABDC=ABCD
2 mulcom ABAB=BA
3 2 3adant3 ABCAB=BA
4 3 adantr ABCDD0AB=BA
5 4 oveq1d ABCDD0ABCD=BACD
6 simpl2 ABCDD0B
7 simpl1 ABCDD0A
8 simp3 ABCC
9 8 anim1i ABCDD0CDD0
10 3anass CDD0CDD0
11 9 10 sylibr ABCDD0CDD0
12 divcl CDD0CD
13 11 12 syl ABCDD0CD
14 6 7 13 mulassd ABCDD0BACD=BACD
15 8 adantr ABCDD0C
16 simpr ABCDD0DD0
17 divass ACDD0ACD=ACD
18 7 15 16 17 syl3anc ABCDD0ACD=ACD
19 18 eqcomd ABCDD0ACD=ACD
20 19 oveq2d ABCDD0BACD=BACD
21 14 20 eqtrd ABCDD0BACD=BACD
22 1 5 21 3eqtrd ABCDD0ABDC=BACD