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 - ˙ = dist G
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 - ˙ = dist G
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