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 10729 | . . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
2 | 1 | 3adant1 1126 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
3 | lttr 10719 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
4 | 3 | expcomd 419 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
5 | breq2 5072 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 ↔ 𝐴 < 𝐶)) | |
6 | 5 | biimpd 231 | . . . . 5 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)) |
7 | 6 | a1i 11 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
8 | 4, 7 | jaod 855 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
9 | 2, 8 | sylbid 242 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))) |
10 | 9 | impcomd 414 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 class class class wbr 5068 ℝcr 10538 < clt 10677 ≤ cle 10678 |
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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-resscn 10596 ax-pre-lttri 10613 ax-pre-lttrn 10614 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 |
This theorem is referenced by: ltleletr 10735 ltletri 10770 ltletrd 10802 ltleadd 11125 lediv12a 11535 nngt0 11671 nnrecgt0 11683 elnnnn0c 11945 elnnz1 12011 zltp1le 12035 uz3m2nn 12294 zbtwnre 12349 ledivge1le 12463 addlelt 12506 qbtwnre 12595 xlemul1a 12684 xrsupsslem 12703 zltaddlt1le 12893 elfzodifsumelfzo 13106 ssfzo12bi 13135 elfznelfzo 13145 ceile 13220 swrdswrd 14069 swrdccatin1 14089 repswswrd 14148 sqrlem4 14607 resqrex 14612 caubnd 14720 rlim2lt 14856 cos01gt0 15546 ruclem12 15596 oddge22np1 15700 sadcaddlem 15808 nn0seqcvgd 15916 coprm 16057 prmgaplem7 16395 prmlem1 16443 prmlem2 16455 icoopnst 23545 ovollb2lem 24091 dvcnvrelem1 24616 aaliou 24929 tanord 25124 logdivlti 25205 logdivlt 25206 ftalem2 25653 gausslemma2dlem1a 25943 pntlem3 26187 crctcshwlkn0lem3 27592 nn0prpwlem 33672 isbasisrelowllem1 34638 isbasisrelowllem2 34639 ltflcei 34882 tan2h 34886 poimirlem29 34923 poimirlem32 34926 2xp3dxp2ge1d 39104 stoweidlem26 42318 stoweid 42355 2leaddle2 43505 gbegt5 43933 gbowgt5 43934 sgoldbeven3prm 43955 nnsum4primesodd 43968 nnsum4primesoddALTV 43969 evengpoap3 43971 bgoldbnnsum3prm 43976 cznnring 44234 nn0sumltlt 44405 rege1logbrege0 44625 rege1logbzge0 44626 fllog2 44635 dignn0ldlem 44669 |
Copyright terms: Public domain | W3C validator |