Metamath Proof Explorer

Theorem caovdir

Description: Reverse distributive law. (Contributed by NM, 26-Aug-1995)

Ref Expression
Hypotheses caovdir.1 ⊢ A ∈ V
caovdir.2 ⊢ B ∈ V
caovdir.3 ⊢ C ∈ V
caovdir.com ⊢ x G y = y G x
caovdir.distr ⊢ x G y F z = x G y F x G z
Assertion caovdir ⊢ A F B G C = A G C F B G C

Proof

Step Hyp Ref Expression
1 caovdir.1 ⊢ A ∈ V
2 caovdir.2 ⊢ B ∈ V
3 caovdir.3 ⊢ C ∈ V
4 caovdir.com ⊢ x G y = y G x
5 caovdir.distr ⊢ x G y F z = x G y F x G z
6 3 1 2 5 caovdi ⊢ C G A F B = C G A F C G B
7 ovex ⊢ A F B ∈ V
8 3 7 4 caovcom ⊢ C G A F B = A F B G C
9 3 1 4 caovcom ⊢ C G A = A G C
10 3 2 4 caovcom ⊢ C G B = B G C
11 9 10 oveq12i ⊢ C G A F C G B = A G C F B G C
12 6 8 11 3eqtr3i ⊢ A F B G C = A G C F B G C