Metamath Proof Explorer

Theorem endofsegid

Description: If A , B , and C fall in order on a line, and A B and A C are congruent, then C = B . (Contributed by Scott Fenton, 7-Oct-2013)

Ref Expression
Assertion endofsegid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC∧ACCgrAB→C=B

Proof

Step Hyp Ref Expression
1 simpl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→N∈ℕ
2 simpr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N
3 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C∈𝔼⁡N
4 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B∈𝔼⁡N
5 cgrcom ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→ACCgrAB↔ABCgrAC
6 1 2 3 2 4 5 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ACCgrAB↔ABCgrAC
7 6 biimpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ACCgrAB→ABCgrAC
8 idd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ACCgrAB→ACCgrAB
9 axcgrrflx ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N→BCCgrCB
10 9 3adant3r1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BCCgrCB
11 10 a1d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ACCgrAB→BCCgrCB
12 7 8 11 3jcad ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ACCgrAB→ABCgrAC∧ACCgrAB∧BCCgrCB
13 3ancomb ⊢A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N↔A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N
14 brcgr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N→ABCCgr3ACB↔ABCgrAC∧ACCgrAB∧BCCgrCB
15 13 14 syl3an3br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABCCgr3ACB↔ABCgrAC∧ACCgrAB∧BCCgrCB
16 15 3anidm23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABCCgr3ACB↔ABCgrAC∧ACCgrAB∧BCCgrCB
17 12 16 sylibrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ACCgrAB→ABCCgr3ACB
18 btwnxfr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N→BBtwnAC∧ABCCgr3ACB→CBtwnAB
19 13 18 syl3an3br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC∧ABCCgr3ACB→CBtwnAB
20 19 3anidm23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC∧ABCCgr3ACB→CBtwnAB
21 17 20 sylan2d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC∧ACCgrAB→CBtwnAB
22 simpl ⊢BBtwnAC∧ACCgrAB→BBtwnAC
23 22 a1i ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC∧ACCgrAB→BBtwnAC
24 21 23 jcad ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC∧ACCgrAB→CBtwnAB∧BBtwnAC
25 3anrot ⊢C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N↔A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N
26 btwnswapid2 ⊢N∈ℕ∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→CBtwnAB∧BBtwnAC→C=B
27 25 26 sylan2br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB∧BBtwnAC→C=B
28 24 27 syld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnAC∧ACCgrAB→C=B