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 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d = ( dist ‘ 𝐺 )
tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwnintr.1 ( 𝜑𝐴𝑃 )
tgbtwnintr.2 ( 𝜑𝐵𝑃 )
tgbtwnintr.3 ( 𝜑𝐶𝑃 )
tgbtwnintr.4 ( 𝜑𝐷𝑃 )
tgbtwnexch3.5 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnexch3.6 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion tgbtwnexch3 ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d = ( dist ‘ 𝐺 )
3 tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
5 tgbtwnintr.1 ( 𝜑𝐴𝑃 )
6 tgbtwnintr.2 ( 𝜑𝐵𝑃 )
7 tgbtwnintr.3 ( 𝜑𝐶𝑃 )
8 tgbtwnintr.4 ( 𝜑𝐷𝑃 )
9 tgbtwnexch3.5 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
10 tgbtwnexch3.6 ( 𝜑𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
11 1 2 3 4 5 6 7 9 tgbtwncom ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
12 1 2 3 4 5 7 8 10 tgbtwncom ( 𝜑𝐶 ∈ ( 𝐷 𝐼 𝐴 ) )
13 1 2 3 4 6 7 8 5 11 12 tgbtwnintr ( 𝜑𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )