Theorem letri3d 10582

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

Step	Hyp	Ref	Expression
1		ltd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		letri3 10526	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
4	1, 2, 3	syl2anc 576	1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))

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