MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  letri3d Structured version   Visualization version   GIF version

Theorem letri3d 11304
Description: Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
Assertion
Ref Expression
letri3d (𝜑 → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))

Proof of Theorem letri3d
StepHypRef Expression
1 ltd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltd.2 . 2 (𝜑𝐵 ∈ ℝ)
3 letri3 11247 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107   class class class wbr 5110  cr 11057  cle 11197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11115  ax-pre-lttri 11132  ax-pre-lttrn 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202
This theorem is referenced by:  add20  11674  eqord1  11690  msq11  12063  supadd  12130  supmul  12134  suprzcl  12590  uzwo3  12875  flid  13720  flval3  13727  gcd0id  16406  gcdneg  16409  bezoutlem4  16430  gcdzeq  16440  lcmneg  16486  coprmgcdb  16532  qredeq  16540  pcidlem  16751  pcgcd1  16756  4sqlem17  16840  0ram  16899  ram0  16901  mndodconglem  19330  sylow1lem5  19391  zntoslem  20979  cnmpopc  24307  ovolsca  24895  ismbl2  24907  voliunlem2  24931  dyadmaxlem  24977  mbfi1fseqlem4  25099  itg2cnlem1  25142  ditgneg  25237  rolle  25370  dvivthlem1  25388  plyeq0lem  25587  dgreq  25621  coemulhi  25631  dgradd2  25645  dgrmul  25647  plydiveu  25674  vieta1lem2  25687  pilem3  25828  zabsle1  26660  2sqmod  26800  ostth2  27001  brbtwn2  27896  axcontlem8  27962  nmophmi  31015  leoptri  31120  fzto1st1  31993  ballotlemfc0  33132  ballotlemfcc  33133  0nn0m1nnn0  33743  poimirlem23  36130  rmspecfund  41261  ubelsupr  43299  lefldiveq  43600  wallispilem3  44382  fourierdlem6  44428  fourierdlem42  44464  fourierdlem50  44471  fourierdlem52  44473  fourierdlem54  44475  fourierdlem79  44500  fourierdlem102  44523  fourierdlem114  44535  2ffzoeq  45634  lighneallem2  45872
  Copyright terms: Public domain W3C validator