caovcanrd

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

	Ref	Expression
Hypotheses	caovcang.1	$⊢ (φ \land (x \in T \land y \in S \land z \in S)) \to (x F y = x F z \leftrightarrow y = z)$
	caovcand.2	$⊢ φ \to A \in T$
	caovcand.3	$⊢ φ \to B \in S$
	caovcand.4	$⊢ φ \to C \in S$
	caovcanrd.5	$⊢ φ \to A \in S$
	caovcanrd.6	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
Assertion	caovcanrd	$⊢ φ \to (B F A = C F A \leftrightarrow B = C)$

Step	Hyp	Ref	Expression
1		caovcang.1	$⊢ (φ \land (x \in T \land y \in S \land z \in S)) \to (x F y = x F z \leftrightarrow y = z)$
2		caovcand.2	$⊢ φ \to A \in T$
3		caovcand.3	$⊢ φ \to B \in S$
4		caovcand.4	$⊢ φ \to C \in S$
5		caovcanrd.5	$⊢ φ \to A \in S$
6		caovcanrd.6	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
7	6 5 3	caovcomd	$⊢ φ \to A F B = B F A$
8	6 5 4	caovcomd	$⊢ φ \to A F C = C F A$
9	7 8	eqeq12d	$⊢ φ \to (A F B = A F C \leftrightarrow B F A = C F A)$
10	1 2 3 4	caovcand	$⊢ φ \to (A F B = A F C \leftrightarrow B = C)$
11	9 10	bitr3d	$⊢ φ \to (B F A = C F A \leftrightarrow B = C)$

Metamath Proof Explorer