Metamath Proof Explorer


Theorem colinearperm4

Description: Permutation law for colinearity. Part of theorem 4.11 of Schwabhauser p. 36. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion colinearperm4 N A 𝔼 N B 𝔼 N C 𝔼 N A Colinear B C C Colinear A B

Proof

Step Hyp Ref Expression
1 colinearperm3 N A 𝔼 N B 𝔼 N C 𝔼 N A Colinear B C B Colinear C A
2 3anrot A 𝔼 N B 𝔼 N C 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N
3 colinearperm3 N B 𝔼 N C 𝔼 N A 𝔼 N B Colinear C A C Colinear A B
4 2 3 sylan2b N A 𝔼 N B 𝔼 N C 𝔼 N B Colinear C A C Colinear A B
5 1 4 bitrd N A 𝔼 N B 𝔼 N C 𝔼 N A Colinear B C C Colinear A B