Theorem caovcanrd

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

	Ref	Expression
Hypotheses	caovcang.1	$$⊢\left(\phi \wedge \left(x\in T\wedge y\in S\wedge z\in S\right)\right)\to \left(xFy=xFz\leftrightarrow y=z\right)$$
	caovcand.2	$$⊢\phi \to A\in T$$
	caovcand.3	$$⊢\phi \to B\in S$$
	caovcand.4	$$⊢\phi \to C\in S$$
	caovcanrd.5	$$⊢\phi \to A\in S$$
	caovcanrd.6	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy=yFx$$
Assertion	caovcanrd	$$⊢\phi \to \left(BFA=CFA\leftrightarrow B=C\right)$$

Proof

Step	Hyp	Ref	Expression
1		caovcang.1	$$⊢\left(\phi \wedge \left(x\in T\wedge y\in S\wedge z\in S\right)\right)\to \left(xFy=xFz\leftrightarrow y=z\right)$$
2		caovcand.2	$$⊢\phi \to A\in T$$
3		caovcand.3	$$⊢\phi \to B\in S$$
4		caovcand.4	$$⊢\phi \to C\in S$$
5		caovcanrd.5	$$⊢\phi \to A\in S$$
6		caovcanrd.6	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to xFy=yFx$$
7	6 5 3	caovcomd	$$⊢\phi \to AFB=BFA$$
8	6 5 4	caovcomd	$$⊢\phi \to AFC=CFA$$
9	7 8	eqeq12d	$$⊢\phi \to \left(AFB=AFC\leftrightarrow BFA=CFA\right)$$
10	1 2 3 4	caovcand	$$⊢\phi \to \left(AFB=AFC\leftrightarrow B=C\right)$$
11	9 10	bitr3d	$$⊢\phi \to \left(BFA=CFA\leftrightarrow B=C\right)$$