Description: If a point is moved by exactly one of two permutations, then it will be moved by their composite. (Contributed by Stefan O'Rear, 23-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | f1omvdco3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notbi | |
|
2 | disjsn | |
|
3 | disj2 | |
|
4 | 2 3 | bitr3i | |
5 | disjsn | |
|
6 | disj2 | |
|
7 | 5 6 | bitr3i | |
8 | 4 7 | bibi12i | |
9 | 1 8 | bitri | |
10 | 9 | notbii | |
11 | df-xor | |
|
12 | df-xor | |
|
13 | 10 11 12 | 3bitr4i | |
14 | f1omvdco2 | |
|
15 | disj2 | |
|
16 | disjsn | |
|
17 | 15 16 | bitr3i | |
18 | 17 | con2bii | |
19 | 14 18 | sylibr | |
20 | 13 19 | syl3an3b | |