Theorem letri3d 11264

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 11207	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   class class class wbr 5095  ℝcr 11014   ≤ cle 11156

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-resscn 11072  ax-pre-lttri 11089  ax-pre-lttrn 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161

This theorem is referenced by:  add20  11638  eqord1  11654  msq11  12032  supadd  12099  supmul  12103  suprzcl  12561  uzwo3  12845  flid  13716  flval3  13723  gcd0id  16434  gcdneg  16437  bezoutlem4  16457  gcdzeq  16467  lcmneg  16518  coprmgcdb  16564  qredeq  16572  pcidlem  16788  pcgcd1  16793  4sqlem17  16877  0ram  16936  ram0  16938  mndodconglem  19457  sylow1lem5  19518  zntoslem  21497  cnmpopc  24852  ovolsca  25446  ismbl2  25458  voliunlem2  25482  dyadmaxlem  25528  mbfi1fseqlem4  25649  itg2cnlem1  25692  ditgneg  25788  rolle  25924  dvivthlem1  25943  plyeq0lem  26145  dgreq  26179  coemulhi  26189  dgradd2  26204  dgrmul  26206  plydiveu  26236  vieta1lem2  26249  pilem3  26393  recxpf1lem  26668  zabsle1  27237  2sqmod  27377  ostth2  27578  brbtwn2  28887  axcontlem8  28953  nmophmi  32015  leoptri  32120  fzto1st1  33080  ballotlemfc0  34529  ballotlemfcc  34530  0nn0m1nnn0  35180  poimirlem23  37706  unitscyglem1  42311  rmspecfund  43029  ubelsupr  45144  lefldiveq  45420  wallispilem3  46192  fourierdlem6  46238  fourierdlem42  46274  fourierdlem50  46281  fourierdlem52  46283  fourierdlem54  46285  fourierdlem79  46310  fourierdlem102  46333  fourierdlem114  46345  2ffzoeq  47454  lighneallem2  47733