brofs2

Description: Change some conditions for outer five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013)

		Ref	Expression
	Assertion	brofs2	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$

Proof

Step	Hyp	Ref	Expression
1		brofs	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
2		simpr1l	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to B Btwn ⟨A, C⟩$
3		simpr2l	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨A, B⟩ Cgr ⟨E, F⟩$
4		simpr1	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩)$
5		simpr2	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
6	4 5	jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
7	6	ex	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)))$
8		simp11	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to N \in ℕ$
9		simp12	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to A \in 𝔼 (N)$
10		simp13	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to B \in 𝔼 (N)$
11		simp21	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to C \in 𝔼 (N)$
12		simp23	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to E \in 𝔼 (N)$
13		simp31	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to F \in 𝔼 (N)$
14		simp32	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to G \in 𝔼 (N)$
15		cgrextend	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)) \to ⟨A, C⟩ Cgr ⟨E, G⟩)$
16	8 9 10 11 12 13 14 15	syl133anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)) \to ⟨A, C⟩ Cgr ⟨E, G⟩)$
17	7 16	syld	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to ⟨A, C⟩ Cgr ⟨E, G⟩)$
18	17	imp	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨A, C⟩ Cgr ⟨E, G⟩$
19		simpr2r	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨B, C⟩ Cgr ⟨F, G⟩$
20	3 18 19	3jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
21	20	ex	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
22		brcgr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
23	8 9 10 11 12 13 14 22	syl133anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
24	21 23	sylibrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩)$
25	24	imp	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩$
26		simpr3	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)$
27	2 25 26	3jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))$
28		simpr1	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to B Btwn ⟨A, C⟩$
29		3simpa	$⊢ (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩)$
30		btwnxfr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N) \land G \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩) \to F Btwn ⟨E, G⟩)$
31	8 9 10 11 12 13 14 30	syl133anc	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩) \to F Btwn ⟨E, G⟩)$
32	29 31	syl5	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \to F Btwn ⟨E, G⟩)$
33	32	imp	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to F Btwn ⟨E, G⟩$
34	28 33	jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩)$
35		3simpb	$⊢ (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
36	23 35	syl6bi	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
37	36	imp	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
38	37	3ad2antr2	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
39		simpr3	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)$
40	34 38 39	3jca	$⊢ (((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))) \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))$
41	27 40	impbida	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)) \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
42	1 41	bitrd	$⊢ ((N \in ℕ \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land E \in 𝔼 (N)) \land (F \in 𝔼 (N) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$

Metamath Proof Explorer

Theorem brofs2

Proof