Theorem gtneii 11245

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

Syntax hints:   ∈ wcel 2113   ≠ wne 2932   class class class wbr 5098  ℝcr 11025   < clt 11166

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-pre-lttri 11100  ax-pre-lttrn 11101

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171

This theorem is referenced by:  ltneii  11246  fztpval  13502  tpf1ofv2  14421  geo2sum  15796  bpoly4  15982  ene1  16135  3dvds  16258  3lcm2e6  16659  starvndxnbasendx  17224  starvndxnplusgndx  17225  starvndxnmulrndx  17226  scandxnbasendx  17236  scandxnplusgndx  17237  scandxnmulrndx  17238  vscandxnbasendx  17241  vscandxnplusgndx  17242  vscandxnmulrndx  17243  vscandxnscandx  17244  ipndxnbasendx  17252  ipndxnplusgndx  17253  ipndxnmulrndx  17254  tsetndxnbasendx  17276  tsetndxnplusgndx  17277  tsetndxnmulrndx  17278  tsetndxnstarvndx  17279  slotstnscsi  17280  plendxnbasendx  17290  plendxnplusgndx  17291  plendxnmulrndx  17292  plendxnscandx  17293  plendxnvscandx  17294  dsndxnbasendx  17309  dsndxnplusgndx  17310  dsndxnmulrndx  17311  slotsdnscsi  17312  dsndxntsetndx  17313  unifndxnbasendx  17319  unifndxntsetndx  17320  psgnodpmr  21545  logbrec  26748  2logb9irr  26761  2logb3irr  26763  log2le1  26916  2lgsoddprmlem3a  27377  2lgsoddprmlem3b  27378  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  slotsinbpsd  28513  slotslnbpsd  28514  lngndxnitvndx  28515  konigsberglem2  30328  ex-dif  30498  ex-in  30500  ex-pss  30503  ex-res  30516  sgnnbi  32919  sgnpbi  32920  dp20u  32959  dp20h  32960  dp2clq  32962  dp2lt10  32965  dp2lt  32966  dplti  32986  dpexpp1  32989  2sqr3nconstr  33938  cos9thpinconstrlem2  33947  ballotlemi1  34660  signswch  34718  itgexpif  34763  hgt750lemd  34805  hgt750lem  34808  fdc  37946  tan3rdpi  42607  asin1half  42612  areaquad  43458  stirlinglem4  46321  stirlinglem13  46330  stirlinglem14  46331  stirlingr  46334  dirker2re  46336  dirkerdenne0  46337  dirkerre  46339  dirkertrigeqlem1  46342  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem66  46416  fourierdlem83  46433  fourierdlem103  46453  fourierdlem104  46454  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  etransclem46  46524  fmtnoprmfac2lem1  47812  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  usgrexmpl2trifr  48283  zlmodzxzldeplem  48744