![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltlecasei | Structured version Visualization version GIF version |
Description: Ordering elimination by cases. (Contributed by NM, 1-Jul-2007.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
ltlecasei.1 | ⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝜓) |
ltlecasei.2 | ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓) |
ltlecasei.3 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltlecasei.4 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
Ref | Expression |
---|---|
ltlecasei | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltlecasei.2 | . 2 ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓) | |
2 | ltlecasei.1 | . 2 ⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝜓) | |
3 | ltlecasei.4 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
4 | ltlecasei.3 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
5 | lelttric 10434 | . . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ∨ 𝐴 < 𝐵)) | |
6 | 3, 4, 5 | syl2anc 580 | . 2 ⊢ (𝜑 → (𝐵 ≤ 𝐴 ∨ 𝐴 < 𝐵)) |
7 | 1, 2, 6 | mpjaodan 982 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∨ wo 874 ∈ wcel 2157 class class class wbr 4843 ℝcr 10223 < clt 10363 ≤ cle 10364 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pr 5097 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-br 4844 df-opab 4906 df-xp 5318 df-cnv 5320 df-xr 10367 df-le 10369 |
This theorem is referenced by: iccsplit 12559 expnbnd 13247 hashf1 13490 absmax 14410 sinltx 15255 iccntr 22952 pmltpclem2 23557 cniccbdd 23569 iccvolcl 23675 ioovolcl 23678 dyaddisjlem 23703 mbfposr 23760 itg1ge0a 23819 itg2monolem1 23858 itgioo 23923 c1lip1 24101 plyeq0lem 24307 aalioulem5 24432 pserulm 24517 tanord 24626 birthdaylem3 25032 fsumharmonic 25090 chpo1ubb 25522 mblfinlem2 33936 ioodvbdlimc1 40892 ioodvbdlimc2 40894 ibliooicc 40930 fourierdlem107 41173 |
Copyright terms: Public domain | W3C validator |