Theorem lttri 7122

Description: 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
lt.2	⊢ 𝐵 ∈ ℝ
lt.3	⊢ 𝐶 ∈ ℝ

Assertion

Ref	Expression
lttri	⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Proof of Theorem lttri

Step	Hyp	Ref	Expression
1		lt.1	. 2 ⊢ 𝐴 ∈ ℝ
2		lt.2	. 2 ⊢ 𝐵 ∈ ℝ
3		lt.3	. 2 ⊢ 𝐶 ∈ ℝ
4		lttr 7092	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5	1, 2, 3, 4	mp3an 1232	1 ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 97   ∈ wcel 1393   class class class wbr 3764  ℝcr 6888   < clt 7060

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-cnex 6975  ax-resscn 6976  ax-pre-lttrn 6998

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-nel 2207  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-xp 4351  df-pnf 7062  df-mnf 7063  df-ltxr 7065

This theorem is referenced by:  1lt3  8088  2lt4  8090  1lt4  8091  3lt5  8093  2lt5  8094  1lt5  8095  4lt6  8097  3lt6  8098  2lt6  8099  1lt6  8100  5lt7  8102  4lt7  8103  3lt7  8104  2lt7  8105  1lt7  8106  6lt8  8108  5lt8  8109  4lt8  8110  3lt8  8111  2lt8  8112  1lt8  8113  7lt9  8115  6lt9  8116  5lt9  8117  4lt9  8118  3lt9  8119  2lt9  8120  1lt9  8121  8lt10  8123  7lt10  8124  6lt10  8125  5lt10  8126  4lt10  8127  3lt10  8128  2lt10  8129  1lt10  8130