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 AV
caovdi.2 BV
caovdi.3 CV
caovdi.4 xGyFz=xGyFxGz
Assertion caovdi AGBFC=AGBFAGC

Proof

Step Hyp Ref Expression
1 caovdi.1 AV
2 caovdi.2 BV
3 caovdi.3 CV
4 caovdi.4 xGyFz=xGyFxGz
5 tru
6 4 a1i xVyVzVxGyFz=xGyFxGz
7 6 caovdig AVBVCVAGBFC=AGBFAGC
8 5 7 mpan AVBVCVAGBFC=AGBFAGC
9 1 2 3 8 mp3an AGBFC=AGBFAGC