Theorem caovord2d 6139

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 6138	. 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 6126	. . 3 |- ( ph -> ( C F A ) = ( A F C ) )
8	6, 4, 3	caovcomd 6126	. . 3 |- ( ph -> ( C F B ) = ( B F C ) )
9	7, 8	breq12d 4072	. 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 981   = wceq 1373   e. wcel 2178   class class class wbr 4059  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  caovord3d  6140  genplt2i  7658  addnqprllem  7675  addnqprulem  7676  mulnqprl  7716  mulnqpru  7717  distrlem4prl  7732  distrlem4pru  7733  1idprl  7738  1idpru  7739  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemfl  7757  ltexprlemfu  7759  prplnqu  7768  recexprlem1ssl  7781  recexprlem1ssu  7782  aptiprleml  7787  aptiprlemu  7788  caucvgprlemcanl  7792  cauappcvgprlemlol  7795  cauappcvgprlemloc  7800  cauappcvgprlemladdfu  7802  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemlol  7818  caucvgprlemloc  7823  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprprlemnkltj  7837  caucvgprprlemnbj  7841  caucvgprprlemmu  7843  caucvgprprlemlol  7846  caucvgprprlemloc  7851  caucvgprprlemexbt  7854  caucvgprprlemexb  7855  caucvgprprlemaddq  7856  lttrsr  7910  ltsosr  7912  prsrlt  7935  caucvgsrlemoffcau  7946  caucvgsrlemoffgt1  7947  caucvgsrlemoffres  7948  caucvgsr  7950