Metamath Proof Explorer

Theorem btwntriv1

Description: Betweenness always holds for the first endpoint. Theorem 3.3 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwntriv1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnAB

Proof

Step Hyp Ref Expression
1 btwntriv2 ⊢N∈ℕ∧B∈𝔼⁡N∧A∈𝔼⁡N→ABtwnBA
2 1 3com23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnBA
3 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→N∈ℕ
4 simp2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→A∈𝔼⁡N
5 simp3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→B∈𝔼⁡N
6 btwncom ⊢N∈ℕ∧A∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnAB↔ABtwnBA
7 3 4 4 5 6 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnAB↔ABtwnBA
8 2 7 mpbird ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnAB