Theorem caov12 7648

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 7617	. . 3 ⊢ (𝐴𝐹𝐵) = (𝐵𝐹𝐴)
5	4	oveq1i 7429	. 2 ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = ((𝐵𝐹𝐴)𝐹𝐶)
6		caov.3	. . 3 ⊢ 𝐶 ∈ V
7		caov.ass	. . 3 ⊢ ((𝑥𝐹𝑦)𝐹𝑧) = (𝑥𝐹(𝑦𝐹𝑧))
8	1, 2, 6, 7	caovass 7620	. 2 ⊢ ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))
9	2, 1, 6, 7	caovass 7620	. 2 ⊢ ((𝐵𝐹𝐴)𝐹𝐶) = (𝐵𝐹(𝐴𝐹𝐶))
10	5, 8, 9	3eqtr3i 2796	1 ⊢ (𝐴𝐹(𝐵𝐹𝐶)) = (𝐵𝐹(𝐴𝐹𝐶))

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457  (class class class)co 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  caov31  7649  caov4  7651  caovmo  7657  distrnq  10961  ltaddnq  10974  ltexnq  10975  1idpr  11029  prlem934  11033  prlem936  11047  mulcmpblnrlem  11070  ltsosr  11094  0idsr  11097  1idsr  11098  recexsrlem  11103  mulgt0sr  11105  axmulass  11157