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

Theorem caov12 7010
Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
Hypotheses
Ref Expression
caov.1 𝐴 ∈ V
caov.2 𝐵 ∈ V
caov.3 𝐶 ∈ V
caov.com (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
caov.ass ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))
Assertion
Ref Expression
caov12 (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧

Proof of Theorem caov12
StepHypRef Expression
1 caov.1 . . . 4 𝐴 ∈ V
2 caov.2 . . . 4 𝐵 ∈ V
3 caov.com . . . 4 (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
41, 2, 3caovcom 6979 . . 3 (𝐴𝐹𝐵) = (𝐵𝐹𝐴)
54oveq1i 6804 . 2 ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐵𝐹𝐴)𝐹𝐶)
6 caov.3 . . 3 𝐶 ∈ V
7 caov.ass . . 3 ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))
81, 2, 6, 7caovass 6982 . 2 ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))
92, 1, 6, 7caovass 6982 . 2 ((𝐵𝐹𝐴)𝐹𝐶) = (𝐵𝐹(𝐴𝐹𝐶))
105, 8, 93eqtr3i 2801 1 (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wcel 2145  Vcvv 3351  (class class class)co 6794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5995  df-fv 6040  df-ov 6797
This theorem is referenced by:  caov31  7011  caov4  7013  caovmo  7019  distrnq  9986  ltaddnq  9999  ltexnq  10000  1idpr  10054  prlem934  10058  prlem936  10072  mulcmpblnrlem  10094  ltsosr  10118  0idsr  10121  1idsr  10122  recexsrlem  10127  mulgt0sr  10129  axmulass  10181
  Copyright terms: Public domain W3C validator