Theorem caovcanrd

Description: Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Hypotheses	caovcang.1	|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )
	caovcand.2	|- ( ph -> A e. T )
	caovcand.3	|- ( ph -> B e. S )
	caovcand.4	|- ( ph -> C e. S )
	caovcanrd.5	|- ( ph -> A e. S )
	caovcanrd.6	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
Assertion	caovcanrd	|- ( ph -> ( ( B F A ) = ( C F A ) <-> B = C ) )

Proof

Step	Hyp	Ref	Expression
1		caovcang.1	|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )
2		caovcand.2	|- ( ph -> A e. T )
3		caovcand.3	|- ( ph -> B e. S )
4		caovcand.4	|- ( ph -> C e. S )
5		caovcanrd.5	|- ( ph -> A e. S )
6		caovcanrd.6	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
7	6 5 3	caovcomd	|- ( ph -> ( A F B ) = ( B F A ) )
8	6 5 4	caovcomd	|- ( ph -> ( A F C ) = ( C F A ) )
9	7 8	eqeq12d	|- ( ph -> ( ( A F B ) = ( A F C ) <-> ( B F A ) = ( C F A ) ) )
10	1 2 3 4	caovcand	|- ( ph -> ( ( A F B ) = ( A F C ) <-> B = C ) )
11	9 10	bitr3d	|- ( ph -> ( ( B F A ) = ( C F A ) <-> B = C ) )