Theorem rediv23d

Description: A "commutative"/associative law for division. (Contributed by SN, 9-Apr-2026)

	Ref	Expression
Hypotheses	rediv23d.a	$$⊢\phi \to A\in ℝ$$
	rediv23d.b	$$⊢\phi \to B\in ℝ$$
	rediv23d.c	$$⊢\phi \to C\in ℝ$$
	rediv23d.z	$$⊢\phi \to C\ne 0$$
Assertion	rediv23d	Could not format assertion : No typesetting found for |- ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rediv23d.a	$$⊢\phi \to A\in ℝ$$
2		rediv23d.b	$$⊢\phi \to B\in ℝ$$
3		rediv23d.c	$$⊢\phi \to C\in ℝ$$
4		rediv23d.z	$$⊢\phi \to C\ne 0$$
5	3 4	sn-rereccld	Could not format ( ph -> ( 1 /R C ) e. RR ) : No typesetting found for |- ( ph -> ( 1 /R C ) e. RR ) with typecode |-
6	5	recnd	Could not format ( ph -> ( 1 /R C ) e. CC ) : No typesetting found for |- ( ph -> ( 1 /R C ) e. CC ) with typecode |-
7	1	recnd	$$⊢\phi \to A\in ℂ$$
8	2	recnd	$$⊢\phi \to B\in ℂ$$
9	6 7 8	mulassd	Could not format ( ph -> ( ( ( 1 /R C ) x. A ) x. B ) = ( ( 1 /R C ) x. ( A x. B ) ) ) : No typesetting found for |- ( ph -> ( ( ( 1 /R C ) x. A ) x. B ) = ( ( 1 /R C ) x. ( A x. B ) ) ) with typecode |-
10	1 3 4	redivrec2d	Could not format ( ph -> ( A /R C ) = ( ( 1 /R C ) x. A ) ) : No typesetting found for |- ( ph -> ( A /R C ) = ( ( 1 /R C ) x. A ) ) with typecode |-
11	10	oveq1d	Could not format ( ph -> ( ( A /R C ) x. B ) = ( ( ( 1 /R C ) x. A ) x. B ) ) : No typesetting found for |- ( ph -> ( ( A /R C ) x. B ) = ( ( ( 1 /R C ) x. A ) x. B ) ) with typecode |-
12	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
13	12 3 4	redivrec2d	Could not format ( ph -> ( ( A x. B ) /R C ) = ( ( 1 /R C ) x. ( A x. B ) ) ) : No typesetting found for |- ( ph -> ( ( A x. B ) /R C ) = ( ( 1 /R C ) x. ( A x. B ) ) ) with typecode |-
14	9 11 13	3eqtr4rd	Could not format ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) ) : No typesetting found for |- ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) ) with typecode |-