Theorem letri3d 10381

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145   class class class wbr 4786  ℝcr 10137   ≤ cle 10277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-resscn 10195  ax-pre-lttri 10212  ax-pre-lttrn 10213

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282

This theorem is referenced by:  add20  10742  eqord1  10758  msq11  11126  supadd  11193  supmul  11197  suprzcl  11659  uzwo3  11986  flid  12817  flval3  12824  gcd0id  15448  gcdneg  15451  bezoutlem4  15467  gcdzeq  15479  lcmneg  15524  coprmgcdb  15570  qredeq  15578  pcidlem  15783  pcgcd1  15788  4sqlem17  15872  0ram  15931  ram0  15933  mndodconglem  18167  sylow1lem5  18224  zntoslem  20120  cnmpt2pc  22947  ovolsca  23503  ismbl2  23515  voliunlem2  23539  dyadmaxlem  23585  mbfi1fseqlem4  23705  itg2cnlem1  23748  ditgneg  23841  rolle  23973  dvivthlem1  23991  plyeq0lem  24186  dgreq  24220  coemulhi  24230  dgradd2  24244  dgrmul  24246  plydiveu  24273  vieta1lem2  24286  pilem3  24427  pilem3OLD  24428  zabsle1  25242  ostth2  25547  brbtwn2  26006  axcontlem8  26072  nmophmi  29230  leoptri  29335  2sqmod  29988  fzto1st1  30192  ballotlemfc0  30894  ballotlemfcc  30895  poimirlem23  33765  rmspecfund  38000  ubelsupr  39701  lefldiveq  40023  wallispilem3  40801  fourierdlem6  40847  fourierdlem42  40883  fourierdlem50  40890  fourierdlem52  40892  fourierdlem54  40894  fourierdlem79  40919  fourierdlem102  40942  fourierdlem114  40954  2ffzoeq  41866  lighneallem2  42051