Theorem gtneii 11371

Description: 'Less than' implies not equal. (Contributed by Mario Carneiro, 30-Sep-2013.)

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
ltneii.2	⊢ 𝐴 < 𝐵

Assertion

Ref	Expression
gtneii	⊢ 𝐵 ≠ 𝐴

Proof of Theorem gtneii

Step	Hyp	Ref	Expression
1		lt.1	. 2 ⊢ 𝐴 ∈ ℝ
2		ltneii.2	. 2 ⊢ 𝐴 < 𝐵
3		ltne 11356	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
4	1, 2, 3	mp2an 692	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ∈ wcel 2106   ≠ wne 2938   class class class wbr 5148  ℝcr 11152   < clt 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-pre-lttri 11227  ax-pre-lttrn 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-ltxr 11298

This theorem is referenced by:  ltneii  11372  fztpval  13623  tpf1ofv2  14534  geo2sum  15906  bpoly4  16092  ene1  16243  3dvds  16365  3lcm2e6  16766  resslemOLD  17288  starvndxnbasendx  17350  starvndxnplusgndx  17351  starvndxnmulrndx  17352  scandxnbasendx  17362  scandxnplusgndx  17363  scandxnmulrndx  17364  vscandxnbasendx  17367  vscandxnplusgndx  17368  vscandxnmulrndx  17369  vscandxnscandx  17370  ipndxnbasendx  17378  ipndxnplusgndx  17379  ipndxnmulrndx  17380  tsetndxnbasendx  17402  tsetndxnplusgndx  17403  tsetndxnmulrndx  17404  tsetndxnstarvndx  17405  slotstnscsi  17406  plendxnbasendx  17416  plendxnplusgndx  17417  plendxnmulrndx  17418  plendxnscandx  17419  plendxnvscandx  17420  dsndxnbasendx  17435  dsndxnplusgndx  17436  dsndxnmulrndx  17437  slotsdnscsi  17438  dsndxntsetndx  17439  unifndxnbasendx  17445  unifndxntsetndx  17446  resccoOLD  17882  oppgtsetOLD  19386  symgvalstructOLD  19430  mgpscaOLD  20161  mgptsetOLD  20163  mgpdsOLD  20166  cnfldfunALTOLDOLD  21411  psgnodpmr  21626  matscaOLD  22436  matvscaOLD  22438  tuslemOLD  24292  setsmsdsOLD  24504  tngdsOLD  24685  logbrec  26840  2logb9irr  26853  2logb3irr  26855  log2le1  27008  2lgsoddprmlem3a  27469  2lgsoddprmlem3b  27470  2lgsoddprmlem3c  27471  2lgsoddprmlem3d  27472  slotsinbpsd  28464  slotslnbpsd  28465  lngndxnitvndx  28466  konigsberglem2  30282  ex-dif  30452  ex-in  30454  ex-pss  30457  ex-res  30470  dp20u  32845  dp20h  32846  dp2clq  32848  dp2lt10  32851  dp2lt  32852  dplti  32872  dpexpp1  32875  oppgleOLD  32937  resvvscaOLD  33344  zlmdsOLD  33924  zlmtsetOLD  33926  ballotlemi1  34484  sgnnbi  34527  sgnpbi  34528  signswch  34555  itgexpif  34600  hgt750lemd  34642  hgt750lem  34645  fdc  37732  tan3rdpi  42365  asin1half  42366  areaquad  43205  mnringscadOLD  44219  mnringvscadOLD  44221  stirlinglem4  46033  stirlinglem13  46042  stirlinglem14  46043  stirlingr  46046  dirker2re  46048  dirkerdenne0  46049  dirkerre  46051  dirkertrigeqlem1  46054  dirkercncflem2  46060  dirkercncflem4  46062  fourierdlem16  46079  fourierdlem21  46084  fourierdlem22  46085  fourierdlem66  46128  fourierdlem83  46145  fourierdlem103  46165  fourierdlem104  46166  sqwvfoura  46184  sqwvfourb  46185  fourierswlem  46186  fouriersw  46187  etransclem46  46236  fmtnoprmfac2lem1  47491  usgrexmpl2nb3  47929  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  usgrexmpl2trifr  47932  zlmodzxzldeplem  48344