![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > lttr | GIF version |
Description: Alias for axlttrn 7616, for naming consistency with lttri 7650. New proofs should generally use this instead of ax-pre-lttrn 7520. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
lttr | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axlttrn 7616 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 925 ∈ wcel 1439 class class class wbr 3851 ℝcr 7410 < clt 7583 |
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 580 ax-in2 581 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-13 1450 ax-14 1451 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-sep 3963 ax-pow 4015 ax-pr 4045 ax-un 4269 ax-setind 4366 ax-cnex 7497 ax-resscn 7498 ax-pre-lttrn 7520 |
This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-fal 1296 df-nf 1396 df-sb 1694 df-eu 1952 df-mo 1953 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ne 2257 df-nel 2352 df-ral 2365 df-rex 2366 df-rab 2369 df-v 2622 df-dif 3002 df-un 3004 df-in 3006 df-ss 3013 df-pw 3435 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-br 3852 df-opab 3906 df-xp 4458 df-pnf 7585 df-mnf 7586 df-ltxr 7588 |
This theorem is referenced by: ltso 7624 ltleletr 7628 ltnsym 7632 lttri 7650 lttrd 7670 lt2add 7984 lt2sub 7999 mulgt1 8385 recgt1i 8420 recreclt 8422 nnge1 8506 recnz 8900 gtndiv 8902 xrlttr 9326 fzo1fzo0n0 9655 expnbnd 10138 expnlbnd 10139 sin01gt0 11113 cos01gt0 11114 ltoddhalfle 11232 nno 11245 dvdsnprmd 11446 |
Copyright terms: Public domain | W3C validator |