Theorem gtneii 11017

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 11002	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
4	1, 2, 3	mp2an 688	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ∈ wcel 2108   ≠ wne 2942   class class class wbr 5070  ℝcr 10801   < clt 10940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945

This theorem is referenced by:  ltneii  11018  fztpval  13247  geo2sum  15513  bpoly4  15697  ene1  15847  3dvds  15968  3lcm2e6  16364  resslemOLD  16878  starvndxnbasendx  16940  starvndxnplusgndx  16941  starvndxnmulrndx  16942  scandxnbasendx  16952  scandxnplusgndx  16953  scandxnmulrndx  16954  vscandxnbasendx  16957  vscandxnplusgndx  16958  vscandxnmulrndx  16959  vscandxnscandx  16960  ipndxnbasendx  16968  ipndxnplusgndx  16969  ipndxnmulrndx  16970  tsetndxnbasendx  16991  tsetndxnplusgndx  16992  tsetndxnmulrndx  16993  slotstnscsi  16994  plendxnbasendx  17004  plendxnplusgndx  17005  plendxnmulrndx  17006  plendxnscandx  17007  plendxnvscandx  17008  dsndxnbasendx  17020  dsndxnplusgndx  17021  dsndxnmulrndx  17022  slotsdnscsi  17023  dsndxntsetndx  17024  unifndxnbasendx  17029  unifndxntsetndx  17030  resccoOLD  17463  oppgtsetOLD  18874  symgvalstructOLD  18920  mgpscaOLD  19644  mgptsetOLD  19646  mgpdsOLD  19649  cnfldfun  20522  psgnodpmr  20707  matsca  21472  matvsca  21473  tuslemOLD  23327  setsmsds  23537  tngdsOLD  23718  logbrec  25837  2logb9irr  25850  2logb3irr  25852  log2le1  26005  2lgsoddprmlem3a  26463  2lgsoddprmlem3b  26464  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  slotsinbpsd  26707  slotslnbpsd  26708  konigsberglem2  28518  ex-dif  28688  ex-in  28690  ex-pss  28693  ex-res  28706  dp20u  31054  dp20h  31055  dp2clq  31057  dp2lt10  31060  dp2lt  31061  dplti  31081  dpexpp1  31084  oppgleOLD  31141  resvvscaOLD  31439  zlmds  31814  zlmtset  31815  ballotlemi1  32369  sgnnbi  32412  sgnpbi  32413  signswch  32440  itgexpif  32486  hgt750lemd  32528  hgt750lem  32531  fdc  35830  areaquad  40963  mnringscadOLD  41730  mnringvscadOLD  41732  stirlinglem4  43508  stirlinglem13  43517  stirlinglem14  43518  stirlingr  43521  dirker2re  43523  dirkerdenne0  43524  dirkerre  43526  dirkertrigeqlem1  43529  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem66  43603  fourierdlem83  43620  fourierdlem103  43640  fourierdlem104  43641  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  etransclem46  43711  fmtnoprmfac2lem1  44906  zlmodzxzldeplem  45727