Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Geometry in the Euclidean space
Betweenness properties
btwnexch3and
Next ⟩
btwnouttr2
Metamath Proof Explorer
Ascii
Unicode
Theorem
btwnexch3and
Description:
Deduction form of
btwnexch3
.
(Contributed by
Scott Fenton
, 13-Oct-2013)
Ref
Expression
Hypotheses
btwnexch3and.1
⊢
φ
→
N
∈
ℕ
btwnexch3and.2
⊢
φ
→
A
∈
𝔼
⁡
N
btwnexch3and.3
⊢
φ
→
B
∈
𝔼
⁡
N
btwnexch3and.4
⊢
φ
→
C
∈
𝔼
⁡
N
btwnexch3and.5
⊢
φ
→
D
∈
𝔼
⁡
N
btwnexch3and.6
⊢
φ
∧
ψ
→
B
Btwn
A
C
btwnexch3and.7
⊢
φ
∧
ψ
→
C
Btwn
A
D
Assertion
btwnexch3and
⊢
φ
∧
ψ
→
C
Btwn
B
D
Proof
Step
Hyp
Ref
Expression
1
btwnexch3and.1
⊢
φ
→
N
∈
ℕ
2
btwnexch3and.2
⊢
φ
→
A
∈
𝔼
⁡
N
3
btwnexch3and.3
⊢
φ
→
B
∈
𝔼
⁡
N
4
btwnexch3and.4
⊢
φ
→
C
∈
𝔼
⁡
N
5
btwnexch3and.5
⊢
φ
→
D
∈
𝔼
⁡
N
6
btwnexch3and.6
⊢
φ
∧
ψ
→
B
Btwn
A
C
7
btwnexch3and.7
⊢
φ
∧
ψ
→
C
Btwn
A
D
8
btwnexch3
⊢
N
∈
ℕ
∧
A
∈
𝔼
⁡
N
∧
B
∈
𝔼
⁡
N
∧
C
∈
𝔼
⁡
N
∧
D
∈
𝔼
⁡
N
→
B
Btwn
A
C
∧
C
Btwn
A
D
→
C
Btwn
B
D
9
1
2
3
4
5
8
syl122anc
⊢
φ
→
B
Btwn
A
C
∧
C
Btwn
A
D
→
C
Btwn
B
D
10
9
adantr
⊢
φ
∧
ψ
→
B
Btwn
A
C
∧
C
Btwn
A
D
→
C
Btwn
B
D
11
6
7
10
mp2and
⊢
φ
∧
ψ
→
C
Btwn
B
D