This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caovordid

Description: Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014)

	Ref	Expression
Hypotheses	caovordig.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x R y \to (z F x) R (z F y))$
	caovordid.2	$⊢ φ \to A \in S$
	caovordid.3	$⊢ φ \to B \in S$
	caovordid.4	$⊢ φ \to C \in S$
Assertion	caovordid	$⊢ φ \to (A R B \to (C F A) R (C F B))$

Step	Hyp	Ref	Expression
1		caovordig.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x R y \to (z F x) R (z F y))$
2		caovordid.2	$⊢ φ \to A \in S$
3		caovordid.3	$⊢ φ \to B \in S$
4		caovordid.4	$⊢ φ \to C \in S$
5		id	$⊢ φ \to φ$
6	1	caovordig	$⊢ (φ \land (A \in S \land B \in S \land C \in S)) \to (A R B \to (C F A) R (C F B))$
7	5 2 3 4 6	syl13anc	$⊢ φ \to (A R B \to (C F A) R (C F B))$