Theorem gtneii 11308

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

Syntax hints:   ∈ wcel 2106   ≠ wne 2939   class class class wbr 5141  ℝcr 11091   < clt 11230

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-resscn 11149  ax-pre-lttri 11166  ax-pre-lttrn 11167

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-po 5581  df-so 5582  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-er 8686  df-en 8923  df-dom 8924  df-sdom 8925  df-pnf 11232  df-mnf 11233  df-ltxr 11235

This theorem is referenced by:  ltneii  11309  fztpval  13545  geo2sum  15801  bpoly4  15985  ene1  16135  3dvds  16256  3lcm2e6  16650  resslemOLD  17169  starvndxnbasendx  17231  starvndxnplusgndx  17232  starvndxnmulrndx  17233  scandxnbasendx  17243  scandxnplusgndx  17244  scandxnmulrndx  17245  vscandxnbasendx  17248  vscandxnplusgndx  17249  vscandxnmulrndx  17250  vscandxnscandx  17251  ipndxnbasendx  17259  ipndxnplusgndx  17260  ipndxnmulrndx  17261  tsetndxnbasendx  17283  tsetndxnplusgndx  17284  tsetndxnmulrndx  17285  tsetndxnstarvndx  17286  slotstnscsi  17287  plendxnbasendx  17297  plendxnplusgndx  17298  plendxnmulrndx  17299  plendxnscandx  17300  plendxnvscandx  17301  dsndxnbasendx  17316  dsndxnplusgndx  17317  dsndxnmulrndx  17318  slotsdnscsi  17319  dsndxntsetndx  17320  unifndxnbasendx  17326  unifndxntsetndx  17327  resccoOLD  17763  oppgtsetOLD  19183  symgvalstructOLD  19229  mgpscaOLD  19955  mgptsetOLD  19957  mgpdsOLD  19960  cnfldfunALTOLD  20892  psgnodpmr  21076  matscaOLD  21845  matvscaOLD  21847  tuslemOLD  23701  setsmsdsOLD  23913  tngdsOLD  24094  logbrec  26214  2logb9irr  26227  2logb3irr  26229  log2le1  26382  2lgsoddprmlem3a  26840  2lgsoddprmlem3b  26841  2lgsoddprmlem3c  26842  2lgsoddprmlem3d  26843  slotsinbpsd  27557  slotslnbpsd  27558  lngndxnitvndx  27559  konigsberglem2  29371  ex-dif  29541  ex-in  29543  ex-pss  29546  ex-res  29559  dp20u  31915  dp20h  31916  dp2clq  31918  dp2lt10  31921  dp2lt  31922  dplti  31942  dpexpp1  31945  oppgleOLD  32002  resvvscaOLD  32314  zlmdsOLD  32772  zlmtsetOLD  32774  ballotlemi1  33330  sgnnbi  33373  sgnpbi  33374  signswch  33401  itgexpif  33447  hgt750lemd  33489  hgt750lem  33492  fdc  36416  areaquad  41734  mnringscadOLD  42751  mnringvscadOLD  42753  stirlinglem4  44564  stirlinglem13  44573  stirlinglem14  44574  stirlingr  44577  dirker2re  44579  dirkerdenne0  44580  dirkerre  44582  dirkertrigeqlem1  44585  dirkercncflem2  44591  dirkercncflem4  44593  fourierdlem16  44610  fourierdlem21  44615  fourierdlem22  44616  fourierdlem66  44659  fourierdlem83  44676  fourierdlem103  44696  fourierdlem104  44697  sqwvfoura  44715  sqwvfourb  44716  fourierswlem  44717  fouriersw  44718  etransclem46  44767  fmtnoprmfac2lem1  46004  zlmodzxzldeplem  46825