MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gtned Structured version   Visualization version   GIF version

Theorem gtned 10773
Description: 'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltned.2 (𝜑𝐴 < 𝐵)
Assertion
Ref Expression
gtned (𝜑𝐵𝐴)

Proof of Theorem gtned
StepHypRef Expression
1 ltd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltned.2 . 2 (𝜑𝐴 < 𝐵)
3 ltne 10735 . 2 ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵𝐴)
41, 2, 3syl2anc 587 1 (𝜑𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  wne 3014   class class class wbr 5052  cr 10534   < clt 10673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-resscn 10592  ax-pre-lttri 10609  ax-pre-lttrn 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-po 5461  df-so 5462  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508  df-pnf 10675  df-mnf 10676  df-ltxr 10678
This theorem is referenced by:  ltned  10774  seqf1olem1  13414  seqf1olem2  13415  hashfun  13803  abssubne0  14676  rpnnen2lem9  15575  rpnnen2lem11  15577  coe1tmmul2  20912  iccpnfcnv  23555  iccpnfhmeo  23556  pmltpclem2  24059  voliunlem1  24160  dvferm1lem  24593  lhop2  24624  ftc1lem5  24649  vieta1lem2  24913  geolim3  24941  logtayl  25257  atanre  25477  lgamgulmlem2  25621  lgamgulmlem3  25622  perfectlem2  25820  axlowdimlem16  26757  clwwisshclwwslem  27805  frgrogt3nreg  28188  qsidomlem1  31009  esumcvgre  31410  eulerpartlems  31678  hgt750lem  31982  ivthALT  33743  unbdqndv2lem2  33909  knoppndvlem17  33927  poimirlem11  35016  poimirlem12  35017  poimirlem24  35029  lcmineqlem11  39278  3lexlogpow5ineq2  39293  rtprmirr  39436  sn-0ne2  39478  pellfundne1  39750  eliccelioc  42088  fmul01lt1lem1  42156  lptre2pt  42212  cncfiooicclem1  42465  cncfioobdlem  42468  dvnmul  42515  ditgeqiooicc  42532  itgioocnicc  42549  iblcncfioo  42550  wallispilem4  42640  wallispi  42642  wallispi2lem1  42643  wallispi2lem2  42644  wallispi2  42645  stirlinglem5  42650  fourierdlem4  42683  fourierdlem34  42713  fourierdlem41  42720  fourierdlem42  42721  fourierdlem48  42726  fourierdlem49  42727  fourierdlem61  42739  fourierdlem73  42751  fourierdlem75  42753  fourierdlem76  42754  fourierdlem81  42759  fourierdlem82  42760  fourierdlem84  42762  fourierdlem93  42771  fourierdlem111  42789  fouriersw  42803  etransclem35  42841  qndenserrnbllem  42866  nnfoctbdjlem  43024  hoidmvlelem3  43166  hoiqssbllem2  43192  smfmullem1  43353  sfprmdvdsmersenne  44051  lighneallem2  44054  perfectALTVlem2  44170  eenglngeehlnmlem2  45082
  Copyright terms: Public domain W3C validator