MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  caov12 Unicode version

Theorem caov12 6090
Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
Hypotheses
Ref Expression
caov.1  |-  A  e. 
_V
caov.2  |-  B  e. 
_V
caov.3  |-  C  e. 
_V
caov.com  |-  ( x F y )  =  ( y F x )
caov.ass  |-  ( ( x F y ) F z )  =  ( x F ( y F z ) )
Assertion
Ref Expression
caov12  |-  ( A F ( B F C ) )  =  ( B F ( A F C ) )
Distinct variable groups:    x, y,
z, A    x, B, y, z    x, C, y, z    x, F, y, z

Proof of Theorem caov12
StepHypRef Expression
1 caov.1 . . . 4  |-  A  e. 
_V
2 caov.2 . . . 4  |-  B  e. 
_V
3 caov.com . . . 4  |-  ( x F y )  =  ( y F x )
41, 2, 3caovcom 6059 . . 3  |-  ( A F B )  =  ( B F A )
54oveq1i 5910 . 2  |-  ( ( A F B ) F C )  =  ( ( B F A ) F C )
6 caov.3 . . 3  |-  C  e. 
_V
7 caov.ass . . 3  |-  ( ( x F y ) F z )  =  ( x F ( y F z ) )
81, 2, 6, 7caovass 6062 . 2  |-  ( ( A F B ) F C )  =  ( A F ( B F C ) )
92, 1, 6, 7caovass 6062 . 2  |-  ( ( B F A ) F C )  =  ( B F ( A F C ) )
105, 8, 93eqtr3i 2344 1  |-  ( A F ( B F C ) )  =  ( B F ( A F C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1633    e. wcel 1701   _Vcvv 2822  (class class class)co 5900
This theorem is referenced by:  caov31  6091  caov4  6093  caovmo  6099  distrnq  8630  ltaddnq  8643  ltexnq  8644  1idpr  8698  prlem934  8702  prlem936  8716  mulcmpblnrlem  8740  ltsosr  8761  0idsr  8764  1idsr  8765  recexsrlem  8770  mulgt0sr  8772  axmulass  8824
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903
  Copyright terms: Public domain W3C validator