Description: Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ndmov.1 | |
|
ndmov.5 | |
||
Assertion | ndmovass | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ndmov.1 | |
|
2 | ndmov.5 | |
|
3 | 1 2 | ndmovrcl | |
4 | 3 | anim1i | |
5 | df-3an | |
|
6 | 4 5 | sylibr | |
7 | 1 | ndmov | |
8 | 6 7 | nsyl5 | |
9 | 1 2 | ndmovrcl | |
10 | 9 | anim2i | |
11 | 3anass | |
|
12 | 10 11 | sylibr | |
13 | 1 | ndmov | |
14 | 12 13 | nsyl5 | |
15 | 8 14 | eqtr4d | |