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

Theorem caov12 7661
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 7630 . . 3 (𝐴𝐹𝐵) = (𝐵𝐹𝐴)
54oveq1i 7441 . 2 ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐵𝐹𝐴)𝐹𝐶)
6 caov.3 . . 3 𝐶 ∈ V
7 caov.ass . . 3 ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))
81, 2, 6, 7caovass 7633 . 2 ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))
92, 1, 6, 7caovass 7633 . 2 ((𝐵𝐹𝐴)𝐹𝐶) = (𝐵𝐹(𝐴𝐹𝐶))
105, 8, 93eqtr3i 2771 1 (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2106  Vcvv 3478  (class class class)co 7431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434
This theorem is referenced by:  caov31  7662  caov4  7664  caovmo  7670  distrnq  10999  ltaddnq  11012  ltexnq  11013  1idpr  11067  prlem934  11071  prlem936  11085  mulcmpblnrlem  11108  ltsosr  11132  0idsr  11135  1idsr  11136  recexsrlem  11141  mulgt0sr  11143  axmulass  11195
  Copyright terms: Public domain W3C validator