Metamath Proof Explorer

Theorem caov4

Description: Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995)

Ref Expression
Hypotheses caov.1 ⊢ A ∈ V
caov.2 ⊢ B ∈ V
caov.3 ⊢ C ∈ V
caov.com ⊢ x F y = y F x
caov.ass ⊢ x F y F z = x F y F z
caov.4 ⊢ D ∈ V
Assertion caov4 ⊢ A F B F C F D = A F C F B F D

Proof

Step Hyp Ref Expression
1 caov.1 ⊢ A ∈ V
2 caov.2 ⊢ B ∈ V
3 caov.3 ⊢ C ∈ V
4 caov.com ⊢ x F y = y F x
5 caov.ass ⊢ x F y F z = x F y F z
6 caov.4 ⊢ D ∈ V
7 2 3 6 4 5 caov12 ⊢ B F C F D = C F B F D
8 7 oveq2i ⊢ A F B F C F D = A F C F B F D
9 ovex ⊢ C F D ∈ V
10 1 2 9 5 caovass ⊢ A F B F C F D = A F B F C F D
11 ovex ⊢ B F D ∈ V
12 1 3 11 5 caovass ⊢ A F C F B F D = A F C F B F D
13 8 10 12 3eqtr4i ⊢ A F B F C F D = A F C F B F D