brifs2

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

		Ref	Expression
	Assertion	brifs2	$⊢ ((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⟩⟩ InnerFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$

Proof

Step	Hyp	Ref	Expression
1		brifs	$⊢ ((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⟩⟩ InnerFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, 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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to B Btwn ⟨A, C⟩$
3		3simpa	$⊢ ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
4		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 ℕ$
5		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)$
6		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)$
7		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)$
8		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)$
9		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)$
10		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)$
11		cgrsub	$⊢ (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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)) \to ⟨A, B⟩ Cgr ⟨E, F⟩)$
12	4 5 6 7 8 9 10 11	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)) \to ⟨A, B⟩ Cgr ⟨E, F⟩)$
13	3 12	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 F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨A, B⟩ Cgr ⟨E, F⟩)$
14	13	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨A, B⟩ Cgr ⟨E, F⟩$
15		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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨A, C⟩ Cgr ⟨E, G⟩$
16		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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨B, C⟩ Cgr ⟨F, G⟩$
17	14 15 16	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
18	17	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
19		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⟩))$
20	4 5 6 7 8 9 10 19	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⟩))$
21	18 20	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩)$
22	21	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩$
23		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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)$
24	2 22 23	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))) \to (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))$
25		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 ⟨C, D⟩ Cgr ⟨G, H⟩))) \to B Btwn ⟨A, C⟩$
26		3simpa	$⊢ (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \to (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩)$
27		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⟩)$
28	4 5 6 7 8 9 10 27	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⟩)$
29	26 28	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 ⟨C, D⟩ Cgr ⟨G, H⟩)) \to F Btwn ⟨E, G⟩)$
30	29	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 ⟨C, D⟩ Cgr ⟨G, H⟩))) \to F Btwn ⟨E, G⟩$
31	25 30	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 ⟨C, D⟩ Cgr ⟨G, H⟩))) \to (B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩)$
32		3simpc	$⊢ (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \to (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
33	20 32	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
34	33	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
35	34	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 ⟨C, D⟩ Cgr ⟨G, H⟩))) \to (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩)$
36		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 ⟨C, D⟩ Cgr ⟨G, H⟩))) \to (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)$
37	31 35 36	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 ⟨C, D⟩ Cgr ⟨G, H⟩))) \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩))$
38	24 37	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, C⟩ Cgr ⟨E, G⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)) \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$
39	1 38	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⟩⟩ InnerFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, ⟨B, C⟩⟩ Cgr3 ⟨E, ⟨F, G⟩⟩ \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨C, D⟩ Cgr ⟨G, H⟩)))$

Metamath Proof Explorer

Theorem brifs2

Proof