Theorem caovord2d 6259

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

Hypotheses

Ref	Expression
caovordg.1	|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )
caovordd.2	|- ( ph -> A e. S )
caovordd.3	|- ( ph -> B e. S )
caovordd.4	|- ( ph -> C e. S )
caovord2d.com	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )

Assertion

Ref	Expression
caovord2d	|- ( ph -> ( A R B <-> ( A F C ) R ( B F C ) ) )

Distinct variable groups:   x, y, z, A   x, B, y, z   x, C, y, z   ph, x, y, z   x, F, y, z   x, R, y, z   x, S, y, z

Proof of Theorem caovord2d

Step	Hyp	Ref	Expression
1		caovordg.1	. . 3 |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )
2		caovordd.2	. . 3 |- ( ph -> A e. S )
3		caovordd.3	. . 3 |- ( ph -> B e. S )
4		caovordd.4	. . 3 |- ( ph -> C e. S )
5	1, 2, 3, 4	caovordd 6258	. 2 |- ( ph -> ( A R B <-> ( C F A ) R ( C F B ) ) )
6		caovord2d.com	. . . 4 |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
7	6, 4, 2	caovcomd 6246	. . 3 |- ( ph -> ( C F A ) = ( A F C ) )
8	6, 4, 3	caovcomd 6246	. . 3 |- ( ph -> ( C F B ) = ( B F C ) )
9	7, 8	breq12d 4143	. 2 |- ( ph -> ( ( C F A ) R ( C F B ) <-> ( A F C ) R ( B F C ) ) )
10	5, 9	bitrd 188	1 |- ( ph -> ( A R B <-> ( A F C ) R ( B F C ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009   = wceq 1402   e. wcel 2209   class class class wbr 4130  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  caovord3d  6260  genplt2i  7878  addnqprllem  7895  addnqprulem  7896  mulnqprl  7936  mulnqpru  7937  distrlem4prl  7952  distrlem4pru  7953  1idprl  7958  1idpru  7959  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemfu  7979  prplnqu  7988  recexprlem1ssl  8001  recexprlem1ssu  8002  aptiprleml  8007  aptiprlemu  8008  caucvgprlemcanl  8012  cauappcvgprlemlol  8015  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemlol  8038  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprprlemnkltj  8057  caucvgprprlemnbj  8061  caucvgprprlemmu  8063  caucvgprprlemlol  8066  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlemexb  8075  caucvgprprlemaddq  8076  lttrsr  8130  ltsosr  8132  prsrlt  8155  caucvgsrlemoffcau  8166  caucvgsrlemoffgt1  8167  caucvgsrlemoffres  8168  caucvgsr  8170