Theorem divdiv23zi

Description: Swap denominators in a division. (Contributed by NM, 15-Sep-1999)

	Ref	Expression
Hypotheses	divclz.1	|- A e. CC
	divclz.2	|- B e. CC
	divmulz.3	|- C e. CC
Assertion	divdiv23zi	|- ( ( B =/= 0 /\ C =/= 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )

Proof

Step	Hyp	Ref	Expression
1		divclz.1	|- A e. CC
2		divclz.2	|- B e. CC
3		divmulz.3	|- C e. CC
4		divdiv32	|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
5	1 4	mp3an1	|- ( ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
6	3 5	mpanr1	|- ( ( ( B e. CC /\ B =/= 0 ) /\ C =/= 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )
7	2 6	mpanl1	|- ( ( B =/= 0 /\ C =/= 0 ) -> ( ( A / B ) / C ) = ( ( A / C ) / B ) )