Metamath Proof Explorer


Theorem tgbtwnexch3

Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019)

Ref Expression
Hypotheses tkgeom.p
|- P = ( Base ` G )
tkgeom.d
|- .- = ( dist ` G )
tkgeom.i
|- I = ( Itv ` G )
tkgeom.g
|- ( ph -> G e. TarskiG )
tgbtwnintr.1
|- ( ph -> A e. P )
tgbtwnintr.2
|- ( ph -> B e. P )
tgbtwnintr.3
|- ( ph -> C e. P )
tgbtwnintr.4
|- ( ph -> D e. P )
tgbtwnexch3.5
|- ( ph -> B e. ( A I C ) )
tgbtwnexch3.6
|- ( ph -> C e. ( A I D ) )
Assertion tgbtwnexch3
|- ( ph -> C e. ( B I D ) )

Proof

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 tgbtwnexch3.5
 |-  ( ph -> B e. ( A I C ) )
10 tgbtwnexch3.6
 |-  ( ph -> C e. ( A I D ) )
11 1 2 3 4 5 6 7 9 tgbtwncom
 |-  ( ph -> B e. ( C I A ) )
12 1 2 3 4 5 7 8 10 tgbtwncom
 |-  ( ph -> C e. ( D I A ) )
13 1 2 3 4 6 7 8 5 11 12 tgbtwnintr
 |-  ( ph -> C e. ( B I D ) )