Theorem caov411d 5628

Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)

Hypotheses

Ref	Expression
caovd.1	⊢ (φ → A ∈ 𝑆)
caovd.2	⊢ (φ → B ∈ 𝑆)
caovd.3	⊢ (φ → 𝐶 ∈ 𝑆)
caovd.com	⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))
caovd.ass	⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))
caovd.4	⊢ (φ → 𝐷 ∈ 𝑆)
caovd.cl	⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)

Assertion

Ref	Expression
caov411d	⊢ (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹B)𝐹(A𝐹𝐷)))

Distinct variable groups:   x,y,z,A   x,B,y,z   x,𝐶,y,z   x,𝐷,y,z   φ,x,y,z   x,𝐹,y,z   x,𝑆,y,z

Proof of Theorem caov411d

Step	Hyp	Ref	Expression
1		caovd.2	. . 3 ⊢ (φ → B ∈ 𝑆)
2		caovd.1	. . 3 ⊢ (φ → A ∈ 𝑆)
3		caovd.3	. . 3 ⊢ (φ → 𝐶 ∈ 𝑆)
4		caovd.com	. . 3 ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) = (y𝐹x))
5		caovd.ass	. . 3 ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆 ∧ z ∈ 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))
6		caovd.4	. . 3 ⊢ (φ → 𝐷 ∈ 𝑆)
7		caovd.cl	. . 3 ⊢ ((φ ∧ (x ∈ 𝑆 ∧ y ∈ 𝑆)) → (x𝐹y) ∈ 𝑆)
8	1, 2, 3, 4, 5, 6, 7	caov4d 5627	. 2 ⊢ (φ → ((B𝐹A)𝐹(𝐶𝐹𝐷)) = ((B𝐹𝐶)𝐹(A𝐹𝐷)))
9	4, 1, 2	caovcomd 5599	. . 3 ⊢ (φ → (B𝐹A) = (A𝐹B))
10	9	oveq1d 5470	. 2 ⊢ (φ → ((B𝐹A)𝐹(𝐶𝐹𝐷)) = ((A𝐹B)𝐹(𝐶𝐹𝐷)))
11	4, 1, 3	caovcomd 5599	. . 3 ⊢ (φ → (B𝐹𝐶) = (𝐶𝐹B))
12	11	oveq1d 5470	. 2 ⊢ (φ → ((B𝐹𝐶)𝐹(A𝐹𝐷)) = ((𝐶𝐹B)𝐹(A𝐹𝐷)))
13	8, 10, 12	3eqtr3d 2077	1 ⊢ (φ → ((A𝐹B)𝐹(𝐶𝐹𝐷)) = ((𝐶𝐹B)𝐹(A𝐹𝐷)))

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  (class class class)co 5455

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458

This theorem is referenced by:  ecopovtrn  6139  ecopovtrng  6142  ltsonq  6382  ltanqg  6384  mulextsr1lem  6706