# Metamath Proof Explorer

## Theorem btwnconn1lem9

Description: Lemma for btwnconn1 . Now, a quick use of transitivity to establish congruence on R Q and E D . (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion btwnconn1lem9 ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\right)\to ⟨{R},{Q}⟩\mathrm{Cgr}⟨{E},{D}⟩$

### Proof

Step Hyp Ref Expression
1 simp11 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to {N}\in ℕ$
2 simp33 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to {R}\in 𝔼\left({N}\right)$
3 simp32 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to {Q}\in 𝔼\left({N}\right)$
4 simp2r3 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to {E}\in 𝔼\left({N}\right)$
5 simp2l2 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to {D}\in 𝔼\left({N}\right)$
6 simp2r1 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to {d}\in 𝔼\left({N}\right)$
7 simp31 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to {P}\in 𝔼\left({N}\right)$
8 simpr3r ${⊢}\left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\to ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩$
9 8 ad2antll ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\right)\to ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩$
10 btwnconn1lem8 ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\right)\to ⟨{R},{P}⟩\mathrm{Cgr}⟨{E},{d}⟩$
11 1 2 3 2 7 4 6 9 10 cgrtrand ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\right)\to ⟨{R},{Q}⟩\mathrm{Cgr}⟨{E},{d}⟩$
12 simp1 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to \left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)$
13 simp2l ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)$
14 simp2r ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)$
15 12 13 14 3jca ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)$
16 simpl ${⊢}\left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\to \left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)$
17 simprl ${⊢}\left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\to \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)$
18 16 17 jca ${⊢}\left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\to \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)$
19 btwnconn1lem6 ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\right)\right)\to ⟨{E},{D}⟩\mathrm{Cgr}⟨{E},{d}⟩$
20 15 18 19 syl2an ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\right)\to ⟨{E},{D}⟩\mathrm{Cgr}⟨{E},{d}⟩$
21 1 2 3 4 5 4 6 11 20 cgrtr3and ${⊢}\left(\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge \left(\left({C}\in 𝔼\left({N}\right)\wedge {D}\in 𝔼\left({N}\right)\wedge {c}\in 𝔼\left({N}\right)\right)\wedge \left({d}\in 𝔼\left({N}\right)\wedge {b}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\right)\right)\wedge \left({P}\in 𝔼\left({N}\right)\wedge {Q}\in 𝔼\left({N}\right)\wedge {R}\in 𝔼\left({N}\right)\right)\right)\wedge \left(\left(\left(\left({A}\ne {B}\wedge {B}\ne {C}\wedge {C}\ne {c}\right)\wedge \left({B}\mathrm{Btwn}⟨{A},{C}⟩\wedge {B}\mathrm{Btwn}⟨{A},{D}⟩\right)\right)\wedge \left(\left({D}\mathrm{Btwn}⟨{A},{c}⟩\wedge ⟨{D},{c}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{A},{d}⟩\wedge ⟨{C},{d}⟩\mathrm{Cgr}⟨{C},{D}⟩\right)\right)\wedge \left(\left({c}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{c},{b}⟩\mathrm{Cgr}⟨{C},{B}⟩\right)\wedge \left({d}\mathrm{Btwn}⟨{A},{b}⟩\wedge ⟨{d},{b}⟩\mathrm{Cgr}⟨{D},{B}⟩\right)\right)\right)\wedge \left(\left({E}\mathrm{Btwn}⟨{C},{c}⟩\wedge {E}\mathrm{Btwn}⟨{D},{d}⟩\right)\wedge \left(\left({C}\mathrm{Btwn}⟨{c},{P}⟩\wedge ⟨{C},{P}⟩\mathrm{Cgr}⟨{C},{d}⟩\right)\wedge \left({C}\mathrm{Btwn}⟨{d},{R}⟩\wedge ⟨{C},{R}⟩\mathrm{Cgr}⟨{C},{E}⟩\right)\wedge \left({R}\mathrm{Btwn}⟨{P},{Q}⟩\wedge ⟨{R},{Q}⟩\mathrm{Cgr}⟨{R},{P}⟩\right)\right)\right)\right)\right)\to ⟨{R},{Q}⟩\mathrm{Cgr}⟨{E},{D}⟩$