Theorem mul4i

Description: Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995)

	Ref	Expression
Hypotheses	mul.1	$$⊢A\in ℂ$$
	mul.2	$$⊢B\in ℂ$$
	mul.3	$$⊢C\in ℂ$$
	mul4.4	$$⊢D\in ℂ$$
Assertion	mul4i	$$⊢ABCD=ACBD$$

Proof

Step	Hyp	Ref	Expression
1		mul.1	$$⊢A\in ℂ$$
2		mul.2	$$⊢B\in ℂ$$
3		mul.3	$$⊢C\in ℂ$$
4		mul4.4	$$⊢D\in ℂ$$
5		mul4	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(C\in ℂ\wedge D\in ℂ\right)\right)\to ABCD=ACBD$$
6	1 2 3 4 5	mp4an	$$⊢ABCD=ACBD$$