Theorem gtneii 11350

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

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2957   class class class wbr 5107  ℝcr 11127   < clt 11271

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-pre-lttri 11202  ax-pre-lttrn 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-ltxr 11276

This theorem is used by:  ltneii  11351  fztpval  13645  tpf1ofv2  14567  sgnnbi  15181  sgnpbi  15182  geo2sum  15966  bpoly4  16151  ene1  16304  3dvds  16427  3lcm2e6  16829  starvndxnbasendx  17395  starvndxnplusgndx  17396  starvndxnmulrndx  17397  scandxnbasendx  17407  scandxnplusgndx  17408  scandxnmulrndx  17409  vscandxnbasendx  17412  vscandxnplusgndx  17413  vscandxnmulrndx  17414  vscandxnscandx  17415  ipndxnbasendx  17423  ipndxnplusgndx  17424  ipndxnmulrndx  17425  tsetndxnbasendx  17447  tsetndxnplusgndx  17448  tsetndxnmulrndx  17449  tsetndxnstarvndx  17450  slotstnscsi  17451  plendxnbasendx  17461  plendxnplusgndx  17462  plendxnmulrndx  17463  plendxnscandx  17464  plendxnvscandx  17465  dsndxnbasendx  17480  dsndxnplusgndx  17481  dsndxnmulrndx  17482  slotsdnscsi  17483  dsndxntsetndx  17484  unifndxnbasendx  17490  unifndxntsetndx  17491  psgnodpmr  21809  logbrec  27027  2logb9irr  27040  2logb3irr  27042  log2le1  27195  2lgsoddprmlem3a  27654  2lgsoddprmlem3b  27655  2lgsoddprmlem3c  27656  2lgsoddprmlem3d  27657  slotsinbpsd  28790  slotslnbpsd  28791  lngndxnitvndx  28792  konigsberglem2  30741  ex-dif  30911  ex-in  30913  ex-pss  30916  ex-res  30929  dp20u  33331  dp20h  33332  dp2clq  33334  dp2lt10  33337  dp2lt  33338  dplti  33358  dpexpp1  33361  2sqr3nconstr  34299  cos9thpinconstrlem2  34308  ballotlemi1  35022  signswch  35077  itgexpif  35122  hgt750lemd  35164  hgt750lem  35167  fdc  38503  tan3rdpi  43235  asin1half  43240  areaquad  44065  stirlinglem4  46913  stirlinglem13  46922  stirlinglem14  46923  stirlingr  46926  dirker2re  46928  dirkerdenne0  46929  dirkerre  46931  dirkertrigeqlem1  46934  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem16  46959  fourierdlem21  46964  fourierdlem22  46965  fourierdlem66  47008  fourierdlem83  47025  fourierdlem103  47045  fourierdlem104  47046  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  etransclem46  47116  numtowerdt  47742  goldratval  47762  fmtnoprmfac2lem1  48477  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  usgrexmpl2trifr  48961  zlmodzxzldeplem  49436  veronesev4lem  50817  veronesev5lem  50818  veronesev6lem  50819  veronesevrowd  50820