![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > letri3d | Structured version Visualization version GIF version |
Description: Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
Ref | Expression |
---|---|
letri3d | ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | ltd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
3 | letri3 10526 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) | |
4 | 1, 2, 3 | syl2anc 576 | 1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 class class class wbr 4929 ℝcr 10334 ≤ cle 10475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-resscn 10392 ax-pre-lttri 10409 ax-pre-lttrn 10410 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-mpt 5009 df-id 5312 df-po 5326 df-so 5327 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-er 8089 df-en 8307 df-dom 8308 df-sdom 8309 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 |
This theorem is referenced by: add20 10953 eqord1 10969 msq11 11342 supadd 11410 supmul 11414 suprzcl 11875 uzwo3 12157 flid 12993 flval3 13000 gcd0id 15727 gcdneg 15730 bezoutlem4 15746 gcdzeq 15758 lcmneg 15803 coprmgcdb 15849 qredeq 15857 pcidlem 16064 pcgcd1 16069 4sqlem17 16153 0ram 16212 ram0 16214 mndodconglem 18431 sylow1lem5 18488 zntoslem 20405 cnmpopc 23235 ovolsca 23819 ismbl2 23831 voliunlem2 23855 dyadmaxlem 23901 mbfi1fseqlem4 24022 itg2cnlem1 24065 ditgneg 24158 rolle 24290 dvivthlem1 24308 plyeq0lem 24503 dgreq 24537 coemulhi 24547 dgradd2 24561 dgrmul 24563 plydiveu 24590 vieta1lem2 24603 pilem3 24744 zabsle1 25574 2sqmod 25714 ostth2 25915 brbtwn2 26394 axcontlem8 26460 nmophmi 29589 leoptri 29694 fzto1st1 30699 ballotlemfc0 31402 ballotlemfcc 31403 poimirlem23 34362 rmspecfund 38908 ubelsupr 40702 lefldiveq 40994 wallispilem3 41789 fourierdlem6 41835 fourierdlem42 41871 fourierdlem50 41878 fourierdlem52 41880 fourierdlem54 41882 fourierdlem79 41907 fourierdlem102 41930 fourierdlem114 41942 2ffzoeq 42940 lighneallem2 43145 |
Copyright terms: Public domain | W3C validator |