# Metamath Proof Explorer

## Theorem tgbtwncomb

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

Ref Expression
Hypotheses tkgeom.p $⊢ P = Base G$
tkgeom.d
tkgeom.i $⊢ I = Itv ⁡ G$
tkgeom.g $⊢ φ → G ∈ 𝒢 Tarski$
tgbtwntriv2.1 $⊢ φ → A ∈ P$
tgbtwntriv2.2 $⊢ φ → B ∈ P$
tgbtwncomb.3 $⊢ φ → C ∈ P$
Assertion tgbtwncomb $⊢ φ → B ∈ A I C ↔ B ∈ C I A$

### Proof

Step Hyp Ref Expression
1 tkgeom.p $⊢ P = Base G$
2 tkgeom.d
3 tkgeom.i $⊢ I = Itv ⁡ G$
4 tkgeom.g $⊢ φ → G ∈ 𝒢 Tarski$
5 tgbtwntriv2.1 $⊢ φ → A ∈ P$
6 tgbtwntriv2.2 $⊢ φ → B ∈ P$
7 tgbtwncomb.3 $⊢ φ → C ∈ P$
8 4 adantr $⊢ φ ∧ B ∈ A I C → G ∈ 𝒢 Tarski$
9 5 adantr $⊢ φ ∧ B ∈ A I C → A ∈ P$
10 6 adantr $⊢ φ ∧ B ∈ A I C → B ∈ P$
11 7 adantr $⊢ φ ∧ B ∈ A I C → C ∈ P$
12 simpr $⊢ φ ∧ B ∈ A I C → B ∈ A I C$
13 1 2 3 8 9 10 11 12 tgbtwncom $⊢ φ ∧ B ∈ A I C → B ∈ C I A$
14 4 adantr $⊢ φ ∧ B ∈ C I A → G ∈ 𝒢 Tarski$
15 7 adantr $⊢ φ ∧ B ∈ C I A → C ∈ P$
16 6 adantr $⊢ φ ∧ B ∈ C I A → B ∈ P$
17 5 adantr $⊢ φ ∧ B ∈ C I A → A ∈ P$
18 simpr $⊢ φ ∧ B ∈ C I A → B ∈ C I A$
19 1 2 3 14 15 16 17 18 tgbtwncom $⊢ φ ∧ B ∈ C I A → B ∈ A I C$
20 13 19 impbida $⊢ φ → B ∈ A I C ↔ B ∈ C I A$