Description: Any operation is commutative outside its domain, analogous to ndmovcom . (Contributed by Alexander van der Vekens, 26-May-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ndmaov.1 | |
|
Assertion | ndmaovcom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ndmaov.1 | |
|
2 | opelxp | |
|
3 | 1 | eqcomi | |
4 | 3 | eleq2i | |
5 | 2 4 | bitr3i | |
6 | ndmaov | |
|
7 | 5 6 | sylnbi | |
8 | ancom | |
|
9 | opelxp | |
|
10 | 3 | eleq2i | |
11 | 8 9 10 | 3bitr2i | |
12 | ndmaov | |
|
13 | 11 12 | sylnbi | |
14 | 7 13 | eqtr4d | |