| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ltletr | Structured version Visualization version GIF version | ||
| Description: Transitive law. (Contributed by NM, 25-Aug-1999.) |
| Ref | Expression |
|---|---|
| ltletr | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leloe 11205 | . . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
| 2 | 1 | 3adant1 1130 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
| 3 | lttr 11195 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
| 4 | 3 | expcomd 416 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
| 5 | breq2 5097 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 ↔ 𝐴 < 𝐶)) | |
| 6 | 5 | biimpd 229 | . . . . 5 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)) |
| 7 | 6 | a1i 11 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
| 8 | 4, 7 | jaod 859 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
| 9 | 2, 8 | sylbid 240 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
| 10 | 9 | impcomd 411 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 class class class wbr 5093 ℝcr 11011 < clt 11152 ≤ cle 11153 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-resscn 11069 ax-pre-lttri 11086 ax-pre-lttrn 11087 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-br 5094 df-opab 5156 df-mpt 5175 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-pnf 11154 df-mnf 11155 df-xr 11156 df-ltxr 11157 df-le 11158 |
| This theorem is referenced by: ltleletr 11212 ltletri 11247 ltletrd 11279 ltleadd 11606 lediv12a 12021 nngt0 12162 nnrecgt0 12174 elnnnn0c 12432 elnnz1 12504 zltp1le 12528 uz3m2nn 12798 zbtwnre 12850 ledivge1le 12969 addlelt 13012 qbtwnre 13104 xlemul1a 13193 xrsupsslem 13212 zltaddlt1le 13411 elfzodifsumelfzo 13637 ssfzo12bi 13667 elfznelfzo 13679 ceile 13759 swrdswrd 14618 swrdccatin1 14638 repswswrd 14697 01sqrexlem4 15158 resqrex 15163 caubnd 15272 rlim2lt 15410 cos01gt0 16106 ruclem12 16156 oddge22np1 16266 sadcaddlem 16374 nn0seqcvgd 16487 coprm 16628 prmgaplem7 16975 prmlem1 17025 prmlem2 17037 icoopnst 24869 ovollb2lem 25422 dvcnvrelem1 25955 aaliou 26279 tanord 26480 logdivlti 26562 logdivlt 26563 ftalem2 27017 gausslemma2dlem1a 27309 pntlem3 27553 crctcshwlkn0lem3 29797 nn0prpwlem 36373 isbasisrelowllem1 37406 isbasisrelowllem2 37407 ltflcei 37654 tan2h 37658 poimirlem29 37695 poimirlem32 37698 stoweidlem26 46129 stoweid 46166 2leaddle2 47403 gbegt5 47866 gbowgt5 47867 sgoldbeven3prm 47888 nnsum4primesodd 47901 nnsum4primesoddALTV 47902 evengpoap3 47904 bgoldbnnsum3prm 47909 cznnring 48367 nn0sumltlt 48455 rege1logbrege0 48664 rege1logbzge0 48665 fllog2 48674 dignn0ldlem 48708 |
| Copyright terms: Public domain | W3C validator |