| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simprl 771 | . . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐶 ∈ (𝐴𝐼𝑥)) | 
| 2 |  | tkgeom.p | . . . . 5
⊢ 𝑃 = (Base‘𝐺) | 
| 3 |  | tkgeom.d | . . . . 5
⊢  − =
(dist‘𝐺) | 
| 4 |  | tkgeom.i | . . . . 5
⊢ 𝐼 = (Itv‘𝐺) | 
| 5 |  | tkgeom.g | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 6 | 5 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐺 ∈ TarskiG) | 
| 7 |  | tgbtwnintr.3 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 8 | 7 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐶 ∈ 𝑃) | 
| 9 |  | tgbtwnintr.4 | . . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 10 | 9 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐷 ∈ 𝑃) | 
| 11 |  | tgbtwnintr.2 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 12 | 11 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐵 ∈ 𝑃) | 
| 13 |  | simplr 769 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝑥 ∈ 𝑃) | 
| 14 |  | tgbtwnouttr2.1 | . . . . . 6
⊢ (𝜑 → 𝐵 ≠ 𝐶) | 
| 15 | 14 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐵 ≠ 𝐶) | 
| 16 |  | tgbtwnintr.1 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 17 | 16 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐴 ∈ 𝑃) | 
| 18 |  | tgbtwnouttr2.2 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) | 
| 19 | 18 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐵 ∈ (𝐴𝐼𝐶)) | 
| 20 | 2, 3, 4, 6, 17, 12, 8, 13, 19, 1 | tgbtwnexch3 28502 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐶 ∈ (𝐵𝐼𝑥)) | 
| 21 |  | tgbtwnouttr2.3 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷)) | 
| 22 | 21 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐶 ∈ (𝐵𝐼𝐷)) | 
| 23 |  | simprr 773 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → (𝐶 − 𝑥) = (𝐶 − 𝐷)) | 
| 24 |  | eqidd 2738 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → (𝐶 − 𝐷) = (𝐶 − 𝐷)) | 
| 25 | 2, 3, 4, 6, 8, 8, 10, 12, 13, 10, 15, 20, 22, 23, 24 | tgsegconeq 28494 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝑥 = 𝐷) | 
| 26 | 25 | oveq2d 7447 | . . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → (𝐴𝐼𝑥) = (𝐴𝐼𝐷)) | 
| 27 | 1, 26 | eleqtrd 2843 | . 2
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) → 𝐶 ∈ (𝐴𝐼𝐷)) | 
| 28 | 2, 3, 4, 5, 16, 7,
7, 9 | axtgsegcon 28472 | . 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝐶 ∈ (𝐴𝐼𝑥) ∧ (𝐶 − 𝑥) = (𝐶 − 𝐷))) | 
| 29 | 27, 28 | r19.29a 3162 | 1
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) |