Theorem caovord2d 6093

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 6092	. 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 6080	. . 3 |- ( ph -> ( C F A ) = ( A F C ) )
8	6, 4, 3	caovcomd 6080	. . 3 |- ( ph -> ( C F B ) = ( B F C ) )
9	7, 8	breq12d 4046	. 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 ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 980   = wceq 1364   e. wcel 2167   class class class wbr 4033  (class class class)co 5922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  caovord3d  6094  genplt2i  7577  addnqprllem  7594  addnqprulem  7595  mulnqprl  7635  mulnqpru  7636  distrlem4prl  7651  distrlem4pru  7652  1idprl  7657  1idpru  7658  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemfl  7676  ltexprlemfu  7678  prplnqu  7687  recexprlem1ssl  7700  recexprlem1ssu  7701  aptiprleml  7706  aptiprlemu  7707  caucvgprlemcanl  7711  cauappcvgprlemlol  7714  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemlol  7737  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprprlemnkltj  7756  caucvgprprlemnbj  7760  caucvgprprlemmu  7762  caucvgprprlemlol  7765  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  caucvgprprlemexb  7774  caucvgprprlemaddq  7775  lttrsr  7829  ltsosr  7831  prsrlt  7854  caucvgsrlemoffcau  7865  caucvgsrlemoffgt1  7866  caucvgsrlemoffres  7867  caucvgsr  7869