Theorem caov12 7597

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

Step	Hyp	Ref	Expression
1		caov.1	. . . 4 ⊢ 𝐴 ∈ V
2		caov.2	. . . 4 ⊢ 𝐵 ∈ V
3		caov.com	. . . 4 ⊢ (𝑥𝐹𝑦) = (𝑦𝐹𝑥)
4	1, 2, 3	caovcom 7566	. . 3 ⊢ (𝐴𝐹𝐵) = (𝐵𝐹𝐴)
5	4	oveq1i 7379	. 2 ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐵𝐹𝐴)𝐹𝐶)
6		caov.3	. . 3 ⊢ 𝐶 ∈ V
7		caov.ass	. . 3 ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))
8	1, 2, 6, 7	caovass 7569	. 2 ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))
9	2, 1, 6, 7	caovass 7569	. 2 ⊢ ((𝐵𝐹𝐴)𝐹𝐶) = (𝐵𝐹(𝐴𝐹𝐶))
10	5, 8, 9	3eqtr3i 2760	1 ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3444  (class class class)co 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  caov31  7598  caov4  7600  caovmo  7606  distrnq  10890  ltaddnq  10903  ltexnq  10904  1idpr  10958  prlem934  10962  prlem936  10976  mulcmpblnrlem  10999  ltsosr  11023  0idsr  11026  1idsr  11027  recexsrlem  11032  mulgt0sr  11034  axmulass  11086