Description: Reverse distributive law. (Contributed by NM, 26-Aug-1995)
Ref | Expression | ||
---|---|---|---|
Hypotheses | caovdir.1 | |
|
caovdir.2 | |
||
caovdir.3 | |
||
caovdir.com | |
||
caovdir.distr | |
||
Assertion | caovdir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caovdir.1 | |
|
2 | caovdir.2 | |
|
3 | caovdir.3 | |
|
4 | caovdir.com | |
|
5 | caovdir.distr | |
|
6 | 3 1 2 5 | caovdi | |
7 | ovex | |
|
8 | 3 7 4 | caovcom | |
9 | 3 1 4 | caovcom | |
10 | 3 2 4 | caovcom | |
11 | 9 10 | oveq12i | |
12 | 6 8 11 | 3eqtr3i | |