Theorem caovord2d 6128

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 6127	. 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 6115	. . 3 |- ( ph -> ( C F A ) = ( A F C ) )
8	6, 4, 3	caovcomd 6115	. . 3 |- ( ph -> ( C F B ) = ( B F C ) )
9	7, 8	breq12d 4063	. 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 2177   class class class wbr 4050  (class class class)co 5956

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 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-br 4051  df-iota 5240  df-fv 5287  df-ov 5959

This theorem is referenced by:  caovord3d  6129  genplt2i  7638  addnqprllem  7655  addnqprulem  7656  mulnqprl  7696  mulnqpru  7697  distrlem4prl  7712  distrlem4pru  7713  1idprl  7718  1idpru  7719  ltexprlemdisj  7734  ltexprlemloc  7735  ltexprlemfl  7737  ltexprlemfu  7739  prplnqu  7748  recexprlem1ssl  7761  recexprlem1ssu  7762  aptiprleml  7767  aptiprlemu  7768  caucvgprlemcanl  7772  cauappcvgprlemlol  7775  cauappcvgprlemloc  7780  cauappcvgprlemladdfu  7782  cauappcvgprlemladdru  7784  cauappcvgprlemladdrl  7785  cauappcvgprlem1  7787  caucvgprlemnkj  7794  caucvgprlemnbj  7795  caucvgprlemlol  7798  caucvgprlemloc  7803  caucvgprlemladdfu  7805  caucvgprlemladdrl  7806  caucvgprprlemnkltj  7817  caucvgprprlemnbj  7821  caucvgprprlemmu  7823  caucvgprprlemlol  7826  caucvgprprlemloc  7831  caucvgprprlemexbt  7834  caucvgprprlemexb  7835  caucvgprprlemaddq  7836  lttrsr  7890  ltsosr  7892  prsrlt  7915  caucvgsrlemoffcau  7926  caucvgsrlemoffgt1  7927  caucvgsrlemoffres  7928  caucvgsr  7930