outsideoftr

Description: Transitivity law for outsideness. Theorem 6.7 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	outsideoftr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((P OutsideOf ⟨A, B⟩ \land P OutsideOf ⟨B, C⟩) \to P OutsideOf ⟨A, C⟩)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \to A \neq P$
2		simplr	$⊢ ((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \to B \neq P$
3		simprr	$⊢ ((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \to C \neq P$
4	1 2 3	3jca	$⊢ ((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \to (A \neq P \land B \neq P \land C \neq P)$
5		simplr1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (A \neq P \land B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \to A \neq P$
6		simplr3	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (A \neq P \land B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \to C \neq P$
7		df-3an	$⊢ ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩ \land B Btwn ⟨P, C⟩) \leftrightarrow (((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩) \land B Btwn ⟨P, C⟩)$
8		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to N \in ℕ$
9		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to P \in 𝔼 (N)$
10		simp2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to A \in 𝔼 (N)$
11		simp2r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to B \in 𝔼 (N)$
12		simp3l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to C \in 𝔼 (N)$
13		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩ \land B Btwn ⟨P, C⟩)) \to A Btwn ⟨P, B⟩$
14		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩ \land B Btwn ⟨P, C⟩)) \to B Btwn ⟨P, C⟩$
15	8 9 10 11 12 13 14	btwnexchand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩ \land B Btwn ⟨P, C⟩)) \to A Btwn ⟨P, C⟩$
16	15	orcd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩ \land B Btwn ⟨P, C⟩)) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)$
17	7 16	sylan2br	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩) \land B Btwn ⟨P, C⟩)) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)$
18	17	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩)) \to (B Btwn ⟨P, C⟩ \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
19		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩) \land C Btwn ⟨P, B⟩)) \to A Btwn ⟨P, B⟩$
20		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩) \land C Btwn ⟨P, B⟩)) \to C Btwn ⟨P, B⟩$
21		btwnconn3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N)) \land (C \in 𝔼 (N) \land B \in 𝔼 (N))) \to ((A Btwn ⟨P, B⟩ \land C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
22	8 9 10 12 11 21	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((A Btwn ⟨P, B⟩ \land C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
23	22	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩) \land C Btwn ⟨P, B⟩)) \to ((A Btwn ⟨P, B⟩ \land C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
24	19 20 23	mp2and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩) \land C Btwn ⟨P, B⟩)) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)$
25	24	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩)) \to (C Btwn ⟨P, B⟩ \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
26	18 25	jaod	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land A Btwn ⟨P, B⟩)) \to ((B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
27	26	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (A \neq P \land B \neq P \land C \neq P)) \to (A Btwn ⟨P, B⟩ \to ((B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)))$
28		simpll2	$⊢ (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land B Btwn ⟨P, C⟩) \to B \neq P$
29	28	adantl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land B Btwn ⟨P, C⟩)) \to B \neq P$
30	29	necomd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land B Btwn ⟨P, C⟩)) \to P \neq B$
31		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land B Btwn ⟨P, C⟩)) \to B Btwn ⟨P, A⟩$
32		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land B Btwn ⟨P, C⟩)) \to B Btwn ⟨P, C⟩$
33		btwnconn1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land B \in 𝔼 (N)) \land (A \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((P \neq B \land B Btwn ⟨P, A⟩ \land B Btwn ⟨P, C⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
34	8 9 11 10 12 33	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((P \neq B \land B Btwn ⟨P, A⟩ \land B Btwn ⟨P, C⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
35	34	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land B Btwn ⟨P, C⟩)) \to ((P \neq B \land B Btwn ⟨P, A⟩ \land B Btwn ⟨P, C⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
36	30 31 32 35	mp3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land B Btwn ⟨P, C⟩)) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)$
37	36	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩)) \to (B Btwn ⟨P, C⟩ \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
38		df-3an	$⊢ ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩ \land C Btwn ⟨P, B⟩) \leftrightarrow (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land C Btwn ⟨P, B⟩)$
39		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩ \land C Btwn ⟨P, B⟩)) \to C Btwn ⟨P, B⟩$
40		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩ \land C Btwn ⟨P, B⟩)) \to B Btwn ⟨P, A⟩$
41	8 9 12 11 10 39 40	btwnexchand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩ \land C Btwn ⟨P, B⟩)) \to C Btwn ⟨P, A⟩$
42	41	olcd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩ \land C Btwn ⟨P, B⟩)) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)$
43	38 42	sylan2br	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩) \land C Btwn ⟨P, B⟩)) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)$
44	43	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩)) \to (C Btwn ⟨P, B⟩ \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
45	37 44	jaod	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land ((A \neq P \land B \neq P \land C \neq P) \land B Btwn ⟨P, A⟩)) \to ((B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
46	45	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (A \neq P \land B \neq P \land C \neq P)) \to (B Btwn ⟨P, A⟩ \to ((B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)))$
47	27 46	jaod	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (A \neq P \land B \neq P \land C \neq P)) \to ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \to ((B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)))$
48	47	imp32	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (A \neq P \land B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \to (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)$
49	5 6 48	3jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \land (A \neq P \land B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \to (A \neq P \land C \neq P \land (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))$
50	49	exp31	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((A \neq P \land B \neq P \land C \neq P) \to (((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)) \to (A \neq P \land C \neq P \land (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))))$
51	4 50	syl5	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to (((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \to (((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)) \to (A \neq P \land C \neq P \land (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩))))$
52	51	impd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \to (A \neq P \land C \neq P \land (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)))$
53		broutsideof2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)))$
54	8 9 10 11 53	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to (P OutsideOf ⟨A, B⟩ \leftrightarrow (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)))$
55		broutsideof2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (P OutsideOf ⟨B, C⟩ \leftrightarrow (B \neq P \land C \neq P \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)))$
56	8 9 11 12 55	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to (P OutsideOf ⟨B, C⟩ \leftrightarrow (B \neq P \land C \neq P \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)))$
57	54 56	anbi12d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((P OutsideOf ⟨A, B⟩ \land P OutsideOf ⟨B, C⟩) \leftrightarrow ((A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \land (B \neq P \land C \neq P \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))))$
58		df-3an	$⊢ (A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \leftrightarrow ((A \neq P \land B \neq P) \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩))$
59		df-3an	$⊢ (B \neq P \land C \neq P \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)) \leftrightarrow ((B \neq P \land C \neq P) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))$
60	58 59	anbi12i	$⊢ ((A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \land (B \neq P \land C \neq P \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \leftrightarrow (((A \neq P \land B \neq P) \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \land ((B \neq P \land C \neq P) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)))$
61		an4	$⊢ (((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \leftrightarrow (((A \neq P \land B \neq P) \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \land ((B \neq P \land C \neq P) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)))$
62	60 61	bitr4i	$⊢ ((A \neq P \land B \neq P \land (A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩)) \land (B \neq P \land C \neq P \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))) \leftrightarrow (((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩)))$
63	57 62	syl6bb	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((P OutsideOf ⟨A, B⟩ \land P OutsideOf ⟨B, C⟩) \leftrightarrow (((A \neq P \land B \neq P) \land (B \neq P \land C \neq P)) \land ((A Btwn ⟨P, B⟩ \lor B Btwn ⟨P, A⟩) \land (B Btwn ⟨P, C⟩ \lor C Btwn ⟨P, B⟩))))$
64		broutsideof2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land C \in 𝔼 (N))) \to (P OutsideOf ⟨A, C⟩ \leftrightarrow (A \neq P \land C \neq P \land (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)))$
65	8 9 10 12 64	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to (P OutsideOf ⟨A, C⟩ \leftrightarrow (A \neq P \land C \neq P \land (A Btwn ⟨P, C⟩ \lor C Btwn ⟨P, A⟩)))$
66	52 63 65	3imtr4d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((P OutsideOf ⟨A, B⟩ \land P OutsideOf ⟨B, C⟩) \to P OutsideOf ⟨A, C⟩)$

Metamath Proof Explorer

Theorem outsideoftr

Proof