Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-pre-lttrn | GIF version |
Description: Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 7839. (Contributed by NM, 13-Oct-2005.) |
Ref | Expression |
---|---|
ax-pre-lttrn | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . . 4 class 𝐴 | |
2 | cr 7766 | . . . 4 class ℝ | |
3 | 1, 2 | wcel 2141 | . . 3 wff 𝐴 ∈ ℝ |
4 | cB | . . . 4 class 𝐵 | |
5 | 4, 2 | wcel 2141 | . . 3 wff 𝐵 ∈ ℝ |
6 | cC | . . . 4 class 𝐶 | |
7 | 6, 2 | wcel 2141 | . . 3 wff 𝐶 ∈ ℝ |
8 | 3, 5, 7 | w3a 973 | . 2 wff (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) |
9 | cltrr 7771 | . . . . 5 class <ℝ | |
10 | 1, 4, 9 | wbr 3987 | . . . 4 wff 𝐴 <ℝ 𝐵 |
11 | 4, 6, 9 | wbr 3987 | . . . 4 wff 𝐵 <ℝ 𝐶 |
12 | 10, 11 | wa 103 | . . 3 wff (𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) |
13 | 1, 6, 9 | wbr 3987 | . . 3 wff 𝐴 <ℝ 𝐶 |
14 | 12, 13 | wi 4 | . 2 wff ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶) |
15 | 8, 14 | wi 4 | 1 wff ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) |
Colors of variables: wff set class |
This axiom is referenced by: axlttrn 7981 |
Copyright terms: Public domain | W3C validator |