Theorem gtneii 11225

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

Syntax hints:   ∈ wcel 2111   ≠ wne 2928   class class class wbr 5091  ℝcr 11005   < clt 11146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11063  ax-pre-lttri 11080  ax-pre-lttrn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151

This theorem is referenced by:  ltneii  11226  fztpval  13486  tpf1ofv2  14405  geo2sum  15780  bpoly4  15966  ene1  16119  3dvds  16242  3lcm2e6  16643  starvndxnbasendx  17208  starvndxnplusgndx  17209  starvndxnmulrndx  17210  scandxnbasendx  17220  scandxnplusgndx  17221  scandxnmulrndx  17222  vscandxnbasendx  17225  vscandxnplusgndx  17226  vscandxnmulrndx  17227  vscandxnscandx  17228  ipndxnbasendx  17236  ipndxnplusgndx  17237  ipndxnmulrndx  17238  tsetndxnbasendx  17260  tsetndxnplusgndx  17261  tsetndxnmulrndx  17262  tsetndxnstarvndx  17263  slotstnscsi  17264  plendxnbasendx  17274  plendxnplusgndx  17275  plendxnmulrndx  17276  plendxnscandx  17277  plendxnvscandx  17278  dsndxnbasendx  17293  dsndxnplusgndx  17294  dsndxnmulrndx  17295  slotsdnscsi  17296  dsndxntsetndx  17297  unifndxnbasendx  17303  unifndxntsetndx  17304  psgnodpmr  21528  logbrec  26720  2logb9irr  26733  2logb3irr  26735  log2le1  26888  2lgsoddprmlem3a  27349  2lgsoddprmlem3b  27350  2lgsoddprmlem3c  27351  2lgsoddprmlem3d  27352  slotsinbpsd  28420  slotslnbpsd  28421  lngndxnitvndx  28422  konigsberglem2  30231  ex-dif  30401  ex-in  30403  ex-pss  30406  ex-res  30419  sgnnbi  32819  sgnpbi  32820  dp20u  32856  dp20h  32857  dp2clq  32859  dp2lt10  32862  dp2lt  32863  dplti  32883  dpexpp1  32886  2sqr3nconstr  33792  cos9thpinconstrlem2  33801  ballotlemi1  34514  signswch  34572  itgexpif  34617  hgt750lemd  34659  hgt750lem  34662  fdc  37791  tan3rdpi  42391  asin1half  42396  areaquad  43255  stirlinglem4  46121  stirlinglem13  46130  stirlinglem14  46131  stirlingr  46134  dirker2re  46136  dirkerdenne0  46137  dirkerre  46139  dirkertrigeqlem1  46142  dirkercncflem2  46148  dirkercncflem4  46150  fourierdlem16  46167  fourierdlem21  46172  fourierdlem22  46173  fourierdlem66  46216  fourierdlem83  46233  fourierdlem103  46253  fourierdlem104  46254  sqwvfoura  46272  sqwvfourb  46273  fourierswlem  46274  fouriersw  46275  etransclem46  46324  fmtnoprmfac2lem1  47603  usgrexmpl2nb3  48071  usgrexmpl2nb4  48072  usgrexmpl2nb5  48073  usgrexmpl2trifr  48074  zlmodzxzldeplem  48536