![]() |
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 10716 | . . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
2 | 1 | 3adant1 1127 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
3 | lttr 10706 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
4 | 3 | expcomd 420 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
5 | breq2 5034 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 ↔ 𝐴 < 𝐶)) | |
6 | 5 | biimpd 232 | . . . . 5 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)) |
7 | 6 | a1i 11 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
8 | 4, 7 | jaod 856 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
9 | 2, 8 | sylbid 243 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
10 | 9 | impcomd 415 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 class class class wbr 5030 ℝcr 10525 < clt 10664 ≤ cle 10665 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-resscn 10583 ax-pre-lttri 10600 ax-pre-lttrn 10601 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 |
This theorem is referenced by: ltleletr 10722 ltletri 10757 ltletrd 10789 ltleadd 11112 lediv12a 11522 nngt0 11656 nnrecgt0 11668 elnnnn0c 11930 elnnz1 11996 zltp1le 12020 uz3m2nn 12279 zbtwnre 12334 ledivge1le 12448 addlelt 12491 qbtwnre 12580 xlemul1a 12669 xrsupsslem 12688 zltaddlt1le 12883 elfzodifsumelfzo 13098 ssfzo12bi 13127 elfznelfzo 13137 ceile 13212 swrdswrd 14058 swrdccatin1 14078 repswswrd 14137 sqrlem4 14597 resqrex 14602 caubnd 14710 rlim2lt 14846 cos01gt0 15536 ruclem12 15586 oddge22np1 15690 sadcaddlem 15796 nn0seqcvgd 15904 coprm 16045 prmgaplem7 16383 prmlem1 16433 prmlem2 16445 icoopnst 23544 ovollb2lem 24092 dvcnvrelem1 24620 aaliou 24934 tanord 25130 logdivlti 25211 logdivlt 25212 ftalem2 25659 gausslemma2dlem1a 25949 pntlem3 26193 crctcshwlkn0lem3 27598 nn0prpwlem 33783 isbasisrelowllem1 34772 isbasisrelowllem2 34773 ltflcei 35045 tan2h 35049 poimirlem29 35086 poimirlem32 35089 2xp3dxp2ge1d 39387 stoweidlem26 42668 stoweid 42705 2leaddle2 43855 gbegt5 44279 gbowgt5 44280 sgoldbeven3prm 44301 nnsum4primesodd 44314 nnsum4primesoddALTV 44315 evengpoap3 44317 bgoldbnnsum3prm 44322 cznnring 44580 nn0sumltlt 44752 rege1logbrege0 44972 rege1logbzge0 44973 fllog2 44982 dignn0ldlem 45016 |
Copyright terms: Public domain | W3C validator |