Metamath Proof Explorer


Theorem caovdir

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

Ref Expression
Hypotheses caovdir.1 AV
caovdir.2 BV
caovdir.3 CV
caovdir.com xGy=yGx
caovdir.distr xGyFz=xGyFxGz
Assertion caovdir AFBGC=AGCFBGC

Proof

Step Hyp Ref Expression
1 caovdir.1 AV
2 caovdir.2 BV
3 caovdir.3 CV
4 caovdir.com xGy=yGx
5 caovdir.distr xGyFz=xGyFxGz
6 3 1 2 5 caovdi CGAFB=CGAFCGB
7 ovex AFBV
8 3 7 4 caovcom CGAFB=AFBGC
9 3 1 4 caovcom CGA=AGC
10 3 2 4 caovcom CGB=BGC
11 9 10 oveq12i CGAFCGB=AGCFBGC
12 6 8 11 3eqtr3i AFBGC=AGCFBGC