Step |
Hyp |
Ref |
Expression |
1 |
|
tkgeom.p |
|- P = ( Base ` G ) |
2 |
|
tkgeom.d |
|- .- = ( dist ` G ) |
3 |
|
tkgeom.i |
|- I = ( Itv ` G ) |
4 |
|
tkgeom.g |
|- ( ph -> G e. TarskiG ) |
5 |
|
tgbtwnintr.1 |
|- ( ph -> A e. P ) |
6 |
|
tgbtwnintr.2 |
|- ( ph -> B e. P ) |
7 |
|
tgbtwnintr.3 |
|- ( ph -> C e. P ) |
8 |
|
tgbtwnintr.4 |
|- ( ph -> D e. P ) |
9 |
|
tgbtwnexch2.1 |
|- ( ph -> B e. ( A I D ) ) |
10 |
|
tgbtwnexch2.2 |
|- ( ph -> C e. ( B I D ) ) |
11 |
|
simpr |
|- ( ( ph /\ B = C ) -> B = C ) |
12 |
9
|
adantr |
|- ( ( ph /\ B = C ) -> B e. ( A I D ) ) |
13 |
11 12
|
eqeltrrd |
|- ( ( ph /\ B = C ) -> C e. ( A I D ) ) |
14 |
4
|
adantr |
|- ( ( ph /\ B =/= C ) -> G e. TarskiG ) |
15 |
5
|
adantr |
|- ( ( ph /\ B =/= C ) -> A e. P ) |
16 |
6
|
adantr |
|- ( ( ph /\ B =/= C ) -> B e. P ) |
17 |
7
|
adantr |
|- ( ( ph /\ B =/= C ) -> C e. P ) |
18 |
8
|
adantr |
|- ( ( ph /\ B =/= C ) -> D e. P ) |
19 |
|
simpr |
|- ( ( ph /\ B =/= C ) -> B =/= C ) |
20 |
10
|
adantr |
|- ( ( ph /\ B =/= C ) -> C e. ( B I D ) ) |
21 |
9
|
adantr |
|- ( ( ph /\ B =/= C ) -> B e. ( A I D ) ) |
22 |
1 2 3 14 17 16 15 18 20 21
|
tgbtwnintr |
|- ( ( ph /\ B =/= C ) -> B e. ( C I A ) ) |
23 |
1 2 3 14 17 16 15 22
|
tgbtwncom |
|- ( ( ph /\ B =/= C ) -> B e. ( A I C ) ) |
24 |
1 2 3 14 15 16 17 18 19 23 20
|
tgbtwnouttr2 |
|- ( ( ph /\ B =/= C ) -> C e. ( A I D ) ) |
25 |
13 24
|
pm2.61dane |
|- ( ph -> C e. ( A I D ) ) |