Metamath Proof Explorer


Theorem divmuleqd

Description: Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses div1d.1 φA
divcld.2 φB
divmuld.3 φC
divmuldivd.4 φD
divmuldivd.5 φB0
divmuldivd.6 φD0
Assertion divmuleqd φAB=CDAD=CB

Proof

Step Hyp Ref Expression
1 div1d.1 φA
2 divcld.2 φB
3 divmuld.3 φC
4 divmuldivd.4 φD
5 divmuldivd.5 φB0
6 divmuldivd.6 φD0
7 2 5 jca φBB0
8 4 6 jca φDD0
9 divmuleq ACBB0DD0AB=CDAD=CB
10 1 3 7 8 9 syl22anc φAB=CDAD=CB