![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > lelttrd | GIF version |
Description: Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
letrd.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ) |
lelttrd.4 | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
lelttrd.5 | ⊢ (𝜑 → 𝐵 < 𝐶) |
Ref | Expression |
---|---|
lelttrd | ⊢ (𝜑 → 𝐴 < 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lelttrd.4 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵) | |
2 | lelttrd.5 | . 2 ⊢ (𝜑 → 𝐵 < 𝐶) | |
3 | ltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
4 | ltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
5 | letrd.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ) | |
6 | lelttr 7670 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
7 | 3, 4, 5, 6 | syl3anc 1181 | . 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
8 | 1, 2, 7 | mp2and 425 | 1 ⊢ (𝜑 → 𝐴 < 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1445 class class class wbr 3867 ℝcr 7446 < clt 7619 ≤ cle 7620 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-cnex 7533 ax-resscn 7534 ax-pre-ltwlin 7555 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-nel 2358 df-ral 2375 df-rex 2376 df-rab 2379 df-v 2635 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-opab 3922 df-xp 4473 df-cnv 4475 df-pnf 7621 df-mnf 7622 df-xr 7623 df-ltxr 7624 df-le 7625 |
This theorem is referenced by: lt2msq1 8443 ledivp1 8461 suprzclex 8943 btwnapz 8975 ge0p1rp 9264 elfzolt3 9717 exbtwnz 9811 btwnzge0 9856 flltdivnn0lt 9860 modqid 9905 mulqaddmodid 9920 modqsubdir 9949 nn0opthlem2d 10244 bcp1nk 10285 zfz1isolemiso 10359 resqrexlemover 10558 resqrexlemnm 10566 resqrexlemcvg 10567 resqrexlemglsq 10570 resqrexlemga 10571 abslt 10636 abs3lem 10659 fzomaxdiflem 10660 icodiamlt 10728 maxltsup 10766 reccn2ap 10856 expcnvre 11046 absltap 11052 cvgratnnlemfm 11072 cvgratnnlemrate 11073 mertenslemi1 11078 ef01bndlem 11196 sin01bnd 11197 cos01bnd 11198 eirraplem 11213 dvdslelemd 11271 sqrt2irrap 11585 ssblex 12217 qdencn 12620 |
Copyright terms: Public domain | W3C validator |