![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > letrd | GIF version |
Description: Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
letrd.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ) |
letrd.4 | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
letrd.5 | ⊢ (𝜑 → 𝐵 ≤ 𝐶) |
Ref | Expression |
---|---|
letrd | ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | letrd.4 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵) | |
2 | letrd.5 | . 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶) | |
3 | ltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
4 | ltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
5 | letrd.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ) | |
6 | letr 7718 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) | |
7 | 3, 4, 5, 6 | syl3anc 1184 | . 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
8 | 1, 2, 7 | mp2and 427 | 1 ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1448 class class class wbr 3875 ℝcr 7499 ≤ cle 7673 |
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 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390 ax-cnex 7586 ax-resscn 7587 ax-pre-ltwlin 7608 |
This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-nel 2363 df-ral 2380 df-rex 2381 df-rab 2384 df-v 2643 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-br 3876 df-opab 3930 df-xp 4483 df-cnv 4485 df-pnf 7674 df-mnf 7675 df-xr 7676 df-ltxr 7677 df-le 7678 |
This theorem is referenced by: eluzuzle 9184 fzdisj 9673 difelfzle 9752 flqwordi 9902 btwnzge0 9914 flqleceil 9931 modqltm1p1mod 9990 seq3split 10093 iseqf1olemqcl 10100 iseqf1olemnab 10102 iseqf1olemab 10103 seq3f1olemqsumkj 10112 seq3f1olemqsumk 10113 seq3f1olemqsum 10114 bernneq 10253 bernneq3 10255 nn0opthlem2d 10308 faclbnd 10328 facubnd 10332 seq3coll 10426 resqrexlemover 10622 resqrexlemdecn 10624 resqrexlemcalc3 10628 absle 10701 releabs 10708 maxleastb 10826 climsqz 10943 climsqz2 10944 fsum3cvg3 11004 expcnvap0 11110 geolim2 11120 cvgratnnlemabsle 11135 cvgratnnlemfm 11137 cvgratnnlemrate 11138 cvgratz 11140 mertenslem2 11144 eftlub 11194 divalglemnqt 11412 infssuzex 11437 ncoprmgcdne1b 11563 ennnfoneleminc 11716 ennnfonelemkh 11717 strleund 11829 |
Copyright terms: Public domain | W3C validator |