Metamath Proof Explorer


Theorem tgbtwncomb

Description: Betweenness commutes, biconditional version. (Contributed by Thierry Arnoux, 3-Apr-2019)

Ref Expression
Hypotheses tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
tkgeom.d = ( dist ‘ 𝐺 )
tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
tgbtwntriv2.1 ( 𝜑𝐴𝑃 )
tgbtwntriv2.2 ( 𝜑𝐵𝑃 )
tgbtwncomb.3 ( 𝜑𝐶𝑃 )
Assertion tgbtwncomb ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ↔ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 tkgeom.p 𝑃 = ( Base ‘ 𝐺 )
2 tkgeom.d = ( dist ‘ 𝐺 )
3 tkgeom.i 𝐼 = ( Itv ‘ 𝐺 )
4 tkgeom.g ( 𝜑𝐺 ∈ TarskiG )
5 tgbtwntriv2.1 ( 𝜑𝐴𝑃 )
6 tgbtwntriv2.2 ( 𝜑𝐵𝑃 )
7 tgbtwncomb.3 ( 𝜑𝐶𝑃 )
8 4 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
9 5 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴𝑃 )
10 6 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵𝑃 )
11 7 adantr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶𝑃 )
12 simpr ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
13 1 2 3 8 9 10 11 12 tgbtwncom ( ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
14 4 adantr ( ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
15 7 adantr ( ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐶𝑃 )
16 6 adantr ( ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵𝑃 )
17 5 adantr ( ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐴𝑃 )
18 simpr ( ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
19 1 2 3 14 15 16 17 18 tgbtwncom ( ( 𝜑𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
20 13 19 impbida ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ↔ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) )