Theorem letri3d 10058

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  add20  10419  eqord1  10435  msq11  10803  supadd  10868  supmul  10872  suprzcl  11333  uzwo3  11659  flid  12471  flval3  12478  gcd0id  15078  gcdneg  15081  bezoutlem4  15097  gcdzeq  15109  lcmneg  15154  coprmgcdb  15200  qredeq  15209  pcidlem  15414  pcgcd1  15419  4sqlem17  15503  0ram  15562  ram0  15564  mndodconglem  17783  sylow1lem5  17840  zntoslem  19724  cnmpt2pc  22535  ovolsca  23090  ismbl2  23102  voliunlem2  23126  dyadmaxlem  23171  mbfi1fseqlem4  23291  itg2cnlem1  23334  ditgneg  23427  rolle  23557  dvivthlem1  23575  plyeq0lem  23770  dgreq  23804  coemulhi  23814  dgradd2  23828  dgrmul  23830  plydiveu  23857  vieta1lem2  23870  pilem3  24011  zabsle1  24821  ostth2  25126  brbtwn2  25585  axcontlem8  25651  nmophmi  28274  leoptri  28379  2sqmod  28979  fzto1st1  29183  ballotlemfc0  29881  ballotlemfcc  29882  poimirlem23  32602  rmspecfund  36492  ubelsupr  38202  lefldiveq  38446  wallispilem3  38960  fourierdlem6  39006  fourierdlem42  39042  fourierdlem50  39049  fourierdlem52  39051  fourierdlem54  39053  fourierdlem79  39078  fourierdlem102  39101  fourierdlem114  39113  lighneallem2  40061  2ffzoeq  40361