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 B Btwn A C A C Cgr A B 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 A C Cgr A B A B Cgr A C
6 1 2 3 2 4 5 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N A C Cgr A B A B Cgr A C
7 6 biimpd N A 𝔼 N B 𝔼 N C 𝔼 N A C Cgr A B A B Cgr A C
8 idd N A 𝔼 N B 𝔼 N C 𝔼 N A C Cgr A B A C Cgr A B
9 axcgrrflx N B 𝔼 N C 𝔼 N B C Cgr C B
10 9 3adant3r1 N A 𝔼 N B 𝔼 N C 𝔼 N B C Cgr C B
11 10 a1d N A 𝔼 N B 𝔼 N C 𝔼 N A C Cgr A B B C Cgr C B
12 7 8 11 3jcad N A 𝔼 N B 𝔼 N C 𝔼 N A C Cgr A B A B Cgr A C A C Cgr A B B C Cgr C B
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 A B C Cgr3 A C B A B Cgr A C A C Cgr A B B C Cgr C B
15 13 14 syl3an3br N A 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N B 𝔼 N C 𝔼 N A B C Cgr3 A C B A B Cgr A C A C Cgr A B B C Cgr C B
16 15 3anidm23 N A 𝔼 N B 𝔼 N C 𝔼 N A B C Cgr3 A C B A B Cgr A C A C Cgr A B B C Cgr C B
17 12 16 sylibrd N A 𝔼 N B 𝔼 N C 𝔼 N A C Cgr A B A B C Cgr3 A C B
18 btwnxfr N A 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N C 𝔼 N B 𝔼 N B Btwn A C A B C Cgr3 A C B C Btwn A B
19 13 18 syl3an3br N A 𝔼 N B 𝔼 N C 𝔼 N A 𝔼 N B 𝔼 N C 𝔼 N B Btwn A C A B C Cgr3 A C B C Btwn A B
20 19 3anidm23 N A 𝔼 N B 𝔼 N C 𝔼 N B Btwn A C A B C Cgr3 A C B C Btwn A B
21 17 20 sylan2d N A 𝔼 N B 𝔼 N C 𝔼 N B Btwn A C A C Cgr A B C Btwn A B
22 simpl B Btwn A C A C Cgr A B B Btwn A C
23 22 a1i N A 𝔼 N B 𝔼 N C 𝔼 N B Btwn A C A C Cgr A B B Btwn A C
24 21 23 jcad N A 𝔼 N B 𝔼 N C 𝔼 N B Btwn A C A C Cgr A B C Btwn A B B Btwn A C
25 3anrot C 𝔼 N A 𝔼 N B 𝔼 N A 𝔼 N B 𝔼 N C 𝔼 N
26 btwnswapid2 N C 𝔼 N A 𝔼 N B 𝔼 N C Btwn A B B Btwn A C C = B
27 25 26 sylan2br N A 𝔼 N B 𝔼 N C 𝔼 N C Btwn A B B Btwn A C C = B
28 24 27 syld N A 𝔼 N B 𝔼 N C 𝔼 N B Btwn A C A C Cgr A B C = B