Metamath Proof Explorer

Theorem caovdi

Description: Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 28-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 caovdi.1 ⊢ A ∈ V
2 caovdi.2 ⊢ B ∈ V
3 caovdi.3 ⊢ C ∈ V
4 caovdi.4 ⊢ x G y F z = x G y F x G z
5 tru ⊢ ⊤
6 4 a1i ⊢ ⊤ ∧ x ∈ V ∧ y ∈ V ∧ z ∈ V → x G y F z = x G y F x G z
7 6 caovdig ⊢ ⊤ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A G B F C = A G B F A G C
8 5 7 mpan ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A G B F C = A G B F A G C
9 1 2 3 8 mp3an ⊢ A G B F C = A G B F A G C