Theorem gtneii 11310

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

Syntax hints:   ∈ wcel 2145   ≠ wne 2960   class class class wbr 5104  ℝcr 11087   < clt 11231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-pre-lttri 11162  ax-pre-lttrn 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236

This theorem is referenced by:  ltneii  11311  fztpval  13602  tpf1ofv2  14523  sgnnbi  15129  sgnpbi  15130  geo2sum  15915  bpoly4  16101  ene1  16254  3dvds  16377  3lcm2e6  16779  starvndxnbasendx  17345  starvndxnplusgndx  17346  starvndxnmulrndx  17347  scandxnbasendx  17357  scandxnplusgndx  17358  scandxnmulrndx  17359  vscandxnbasendx  17362  vscandxnplusgndx  17363  vscandxnmulrndx  17364  vscandxnscandx  17365  ipndxnbasendx  17373  ipndxnplusgndx  17374  ipndxnmulrndx  17375  tsetndxnbasendx  17397  tsetndxnplusgndx  17398  tsetndxnmulrndx  17399  tsetndxnstarvndx  17400  slotstnscsi  17401  plendxnbasendx  17411  plendxnplusgndx  17412  plendxnmulrndx  17413  plendxnscandx  17414  plendxnvscandx  17415  dsndxnbasendx  17430  dsndxnplusgndx  17431  dsndxnmulrndx  17432  slotsdnscsi  17433  dsndxntsetndx  17434  unifndxnbasendx  17440  unifndxntsetndx  17441  psgnodpmr  21697  logbrec  26901  2logb9irr  26914  2logb3irr  26916  log2le1  27069  2lgsoddprmlem3a  27528  2lgsoddprmlem3b  27529  2lgsoddprmlem3c  27530  2lgsoddprmlem3d  27531  slotsinbpsd  28664  slotslnbpsd  28665  lngndxnitvndx  28666  konigsberglem2  30509  ex-dif  30679  ex-in  30681  ex-pss  30684  ex-res  30697  dp20u  33105  dp20h  33106  dp2clq  33108  dp2lt10  33111  dp2lt  33112  dplti  33132  dpexpp1  33135  2sqr3nconstr  34083  cos9thpinconstrlem2  34092  ballotlemi1  34805  signswch  34860  itgexpif  34905  hgt750lemd  34947  hgt750lem  34950  fdc  38251  tan3rdpi  42968  asin1half  42973  areaquad  43800  stirlinglem4  46650  stirlinglem13  46659  stirlinglem14  46660  stirlingr  46663  dirker2re  46665  dirkerdenne0  46666  dirkerre  46668  dirkertrigeqlem1  46671  dirkercncflem2  46677  dirkercncflem4  46679  fourierdlem16  46696  fourierdlem21  46701  fourierdlem22  46702  fourierdlem66  46745  fourierdlem83  46762  fourierdlem103  46782  fourierdlem104  46783  sqwvfoura  46801  sqwvfourb  46802  fourierswlem  46803  fouriersw  46804  etransclem46  46853  fmtnoprmfac2lem1  48174  usgrexmpl2nb3  48655  usgrexmpl2nb4  48656  usgrexmpl2nb5  48657  usgrexmpl2trifr  48658  zlmodzxzldeplem  49130