Theorem gtneii 11402

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2946   class class class wbr 5166  ℝcr 11183   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329

This theorem is referenced by:  ltneii  11403  fztpval  13646  tpf1ofv2  14547  geo2sum  15921  bpoly4  16107  ene1  16258  3dvds  16379  3lcm2e6  16779  resslemOLD  17301  starvndxnbasendx  17363  starvndxnplusgndx  17364  starvndxnmulrndx  17365  scandxnbasendx  17375  scandxnplusgndx  17376  scandxnmulrndx  17377  vscandxnbasendx  17380  vscandxnplusgndx  17381  vscandxnmulrndx  17382  vscandxnscandx  17383  ipndxnbasendx  17391  ipndxnplusgndx  17392  ipndxnmulrndx  17393  tsetndxnbasendx  17415  tsetndxnplusgndx  17416  tsetndxnmulrndx  17417  tsetndxnstarvndx  17418  slotstnscsi  17419  plendxnbasendx  17429  plendxnplusgndx  17430  plendxnmulrndx  17431  plendxnscandx  17432  plendxnvscandx  17433  dsndxnbasendx  17448  dsndxnplusgndx  17449  dsndxnmulrndx  17450  slotsdnscsi  17451  dsndxntsetndx  17452  unifndxnbasendx  17458  unifndxntsetndx  17459  resccoOLD  17895  oppgtsetOLD  19395  symgvalstructOLD  19439  mgpscaOLD  20170  mgptsetOLD  20172  mgpdsOLD  20175  cnfldfunALTOLDOLD  21416  psgnodpmr  21631  matscaOLD  22441  matvscaOLD  22443  tuslemOLD  24297  setsmsdsOLD  24509  tngdsOLD  24690  logbrec  26843  2logb9irr  26856  2logb3irr  26858  log2le1  27011  2lgsoddprmlem3a  27472  2lgsoddprmlem3b  27473  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  slotsinbpsd  28467  slotslnbpsd  28468  lngndxnitvndx  28469  konigsberglem2  30285  ex-dif  30455  ex-in  30457  ex-pss  30460  ex-res  30473  dp20u  32842  dp20h  32843  dp2clq  32845  dp2lt10  32848  dp2lt  32849  dplti  32869  dpexpp1  32872  oppgleOLD  32934  resvvscaOLD  33329  zlmdsOLD  33909  zlmtsetOLD  33911  ballotlemi1  34467  sgnnbi  34510  sgnpbi  34511  signswch  34538  itgexpif  34583  hgt750lemd  34625  hgt750lem  34628  fdc  37705  tan3rdpi  42338  asin1half  42339  areaquad  43177  mnringscadOLD  44192  mnringvscadOLD  44194  stirlinglem4  45998  stirlinglem13  46007  stirlinglem14  46008  stirlingr  46011  dirker2re  46013  dirkerdenne0  46014  dirkerre  46016  dirkertrigeqlem1  46019  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem66  46093  fourierdlem83  46110  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem46  46201  fmtnoprmfac2lem1  47440  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  zlmodzxzldeplem  48227