Theorem letri3d 11323

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   ≤ cle 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  add20  11697  eqord1  11713  msq11  12091  supadd  12158  supmul  12162  suprzcl  12621  uzwo3  12909  flid  13777  flval3  13784  gcd0id  16496  gcdneg  16499  bezoutlem4  16519  gcdzeq  16529  lcmneg  16580  coprmgcdb  16626  qredeq  16634  pcidlem  16850  pcgcd1  16855  4sqlem17  16939  0ram  16998  ram0  17000  mndodconglem  19478  sylow1lem5  19539  zntoslem  21473  cnmpopc  24829  ovolsca  25423  ismbl2  25435  voliunlem2  25459  dyadmaxlem  25505  mbfi1fseqlem4  25626  itg2cnlem1  25669  ditgneg  25765  rolle  25901  dvivthlem1  25920  plyeq0lem  26122  dgreq  26156  coemulhi  26166  dgradd2  26181  dgrmul  26183  plydiveu  26213  vieta1lem2  26226  pilem3  26370  recxpf1lem  26645  zabsle1  27214  2sqmod  27354  ostth2  27555  brbtwn2  28839  axcontlem8  28905  nmophmi  31967  leoptri  32072  fzto1st1  33066  ballotlemfc0  34491  ballotlemfcc  34492  0nn0m1nnn0  35107  poimirlem23  37644  unitscyglem1  42190  rmspecfund  42904  ubelsupr  45021  lefldiveq  45297  wallispilem3  46072  fourierdlem6  46118  fourierdlem42  46154  fourierdlem50  46161  fourierdlem52  46163  fourierdlem54  46165  fourierdlem79  46190  fourierdlem102  46213  fourierdlem114  46225  2ffzoeq  47332  lighneallem2  47611