Theorem caovord2

Description: Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996)

	Ref	Expression
Hypotheses	caovord.1	|- A e. _V
	caovord.2	|- B e. _V
	caovord.3	|- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )
	caovord2.3	|- C e. _V
	caovord2.com	|- ( x F y ) = ( y F x )
Assertion	caovord2	|- ( C e. S -> ( A R B <-> ( A F C ) R ( B F C ) ) )

Proof

Step	Hyp	Ref	Expression
1		caovord.1	|- A e. _V
2		caovord.2	|- B e. _V
3		caovord.3	|- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )
4		caovord2.3	|- C e. _V
5		caovord2.com	|- ( x F y ) = ( y F x )
6	1 2 3	caovord	|- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )
7	4 1 5	caovcom	|- ( C F A ) = ( A F C )
8	4 2 5	caovcom	|- ( C F B ) = ( B F C )
9	7 8	breq12i	|- ( ( C F A ) R ( C F B ) <-> ( A F C ) R ( B F C ) )
10	6 9	bitrdi	|- ( C e. S -> ( A R B <-> ( A F C ) R ( B F C ) ) )