caovord2d

Description: Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Hypotheses	caovordg.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x R y \leftrightarrow (z F x) R (z F y))$
	caovordd.2	$⊢ φ \to A \in S$
	caovordd.3	$⊢ φ \to B \in S$
	caovordd.4	$⊢ φ \to C \in S$
	caovord2d.com	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
Assertion	caovord2d	$⊢ φ \to (A R B \leftrightarrow (A F C) R (B F C))$

Step	Hyp	Ref	Expression
1		caovordg.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x R y \leftrightarrow (z F x) R (z F y))$
2		caovordd.2	$⊢ φ \to A \in S$
3		caovordd.3	$⊢ φ \to B \in S$
4		caovordd.4	$⊢ φ \to C \in S$
5		caovord2d.com	$⊢ (φ \land (x \in S \land y \in S)) \to x F y = y F x$
6	1 2 3 4	caovordd	$⊢ φ \to (A R B \leftrightarrow (C F A) R (C F B))$
7	5 4 2	caovcomd	$⊢ φ \to C F A = A F C$
8	5 4 3	caovcomd	$⊢ φ \to C F B = B F C$
9	7 8	breq12d	$⊢ φ \to ((C F A) R (C F B) \leftrightarrow (A F C) R (B F C))$
10	6 9	bitrd	$⊢ φ \to (A R B \leftrightarrow (A F C) R (B F C))$

Metamath Proof Explorer