Theorem gtneii 11373

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2940   class class class wbr 5143  ℝcr 11154   < clt 11295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300

This theorem is referenced by:  ltneii  11374  fztpval  13626  tpf1ofv2  14537  geo2sum  15909  bpoly4  16095  ene1  16246  3dvds  16368  3lcm2e6  16769  resslemOLD  17288  starvndxnbasendx  17348  starvndxnplusgndx  17349  starvndxnmulrndx  17350  scandxnbasendx  17360  scandxnplusgndx  17361  scandxnmulrndx  17362  vscandxnbasendx  17365  vscandxnplusgndx  17366  vscandxnmulrndx  17367  vscandxnscandx  17368  ipndxnbasendx  17376  ipndxnplusgndx  17377  ipndxnmulrndx  17378  tsetndxnbasendx  17400  tsetndxnplusgndx  17401  tsetndxnmulrndx  17402  tsetndxnstarvndx  17403  slotstnscsi  17404  plendxnbasendx  17414  plendxnplusgndx  17415  plendxnmulrndx  17416  plendxnscandx  17417  plendxnvscandx  17418  dsndxnbasendx  17433  dsndxnplusgndx  17434  dsndxnmulrndx  17435  slotsdnscsi  17436  dsndxntsetndx  17437  unifndxnbasendx  17443  unifndxntsetndx  17444  symgvalstructOLD  19415  cnfldfunALTOLDOLD  21393  psgnodpmr  21608  matscaOLD  22420  matvscaOLD  22422  tuslemOLD  24276  setsmsdsOLD  24488  tngdsOLD  24669  logbrec  26825  2logb9irr  26838  2logb3irr  26840  log2le1  26993  2lgsoddprmlem3a  27454  2lgsoddprmlem3b  27455  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  slotsinbpsd  28449  slotslnbpsd  28450  lngndxnitvndx  28451  konigsberglem2  30272  ex-dif  30442  ex-in  30444  ex-pss  30447  ex-res  30460  dp20u  32860  dp20h  32861  dp2clq  32863  dp2lt10  32866  dp2lt  32867  dplti  32887  dpexpp1  32890  oppgleOLD  32952  resvvscaOLD  33364  zlmdsOLD  33962  zlmtsetOLD  33964  ballotlemi1  34505  sgnnbi  34548  sgnpbi  34549  signswch  34576  itgexpif  34621  hgt750lemd  34663  hgt750lem  34666  fdc  37752  tan3rdpi  42386  asin1half  42387  areaquad  43228  mnringscadOLD  44242  mnringvscadOLD  44244  stirlinglem4  46092  stirlinglem13  46101  stirlinglem14  46102  stirlingr  46105  dirker2re  46107  dirkerdenne0  46108  dirkerre  46110  dirkertrigeqlem1  46113  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem66  46187  fourierdlem83  46204  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem46  46295  fmtnoprmfac2lem1  47553  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  zlmodzxzldeplem  48415