MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  letri3d Unicode version

Theorem letri3d 9204
Description: Consequence of trichotomy. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1  |-  ( ph  ->  A  e.  RR )
ltd.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
letri3d  |-  ( ph  ->  ( A  =  B  <-> 
( A  <_  B  /\  B  <_  A ) ) )

Proof of Theorem letri3d
StepHypRef Expression
1 ltd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 ltd.2 . 2  |-  ( ph  ->  B  e.  RR )
3 letri3 9149 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  =  B  <-> 
( A  <_  B  /\  B  <_  A ) ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  =  B  <-> 
( A  <_  B  /\  B  <_  A ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   class class class wbr 4204   RRcr 8978    <_ cle 9110
This theorem is referenced by:  add20  9529  eqord1  9544  msq11  9900  supmul  9965  suprzcl  10338  uzwo3  10558  flid  11204  flval3  11210  gcd0id  13011  gcdneg  13014  bezoutlem4  13029  gcdeq  13040  qredeq  13094  pcidlem  13233  pcgcd1  13238  4sqlem17  13317  0ram  13376  ram0  13378  mndodconglem  15167  sylow1lem5  15224  zntoslem  16825  cnmpt2pc  18941  ovolsca  19399  ismbl2  19411  voliunlem2  19433  dyadmaxlem  19477  mbflimsup  19546  mbfi1fseqlem4  19598  itg2cnlem1  19641  ditgneg  19732  rolle  19862  dvivthlem1  19880  plyeq0lem  20117  dgreq  20151  coemulhi  20160  dgradd2  20174  dgrmul  20176  plydiveu  20203  vieta1lem2  20216  pilem3  20357  ostth2  21319  nmophmi  23522  leoptri  23627  ballotlemfc0  24738  ballotlemfcc  24739  brbtwn2  25792  axcontlem8  25858  supadd  26185  rmspecfund  26909  ubelsupr  27605  wallispilem3  27730  swrdccat3b  28106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-resscn 9036  ax-pre-lttri 9053  ax-pre-lttrn 9054
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-po 4495  df-so 4496  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-er 6896  df-en 7101  df-dom 7102  df-sdom 7103  df-pnf 9111  df-mnf 9112  df-xr 9113  df-ltxr 9114  df-le 9115
  Copyright terms: Public domain W3C validator