Description: Commutativity law for outsideness. Theorem 6.6 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | outsideofcom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma | |
|
2 | orcom | |
|
3 | 2 | 3anbi3i | |
4 | 1 3 | bitri | |
5 | 4 | a1i | |
6 | broutsideof2 | |
|
7 | 3ancomb | |
|
8 | broutsideof2 | |
|
9 | 7 8 | sylan2b | |
10 | 5 6 9 | 3bitr4d | |