Theorem gtneii 11452

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

This proof depends on syntax axioms:   ∈ wcel 2147   ≠ wne 2959   class class class wbr 5106  ℝcr 11229   < clt 11373

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-resscn 11287  ax-pre-lttri 11304  ax-pre-lttrn 11305

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-po 5564  df-so 5565  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-ltxr 11378

This theorem is used by:  ltneii  11453  fztpval  13750  tpf1ofv2  14673  sgnnbi  15289  sgnpbi  15290  geo2sum  16074  bpoly4  16257  ene1  16410  3dvds  16533  3lcm2e6  16940  starvndxnbasendx  17507  starvndxnplusgndx  17508  starvndxnmulrndx  17509  scandxnbasendx  17519  scandxnplusgndx  17520  scandxnmulrndx  17521  vscandxnbasendx  17524  vscandxnplusgndx  17525  vscandxnmulrndx  17526  vscandxnscandx  17527  ipndxnbasendx  17535  ipndxnplusgndx  17536  ipndxnmulrndx  17537  tsetndxnbasendx  17559  tsetndxnplusgndx  17560  tsetndxnmulrndx  17561  tsetndxnstarvndx  17562  slotstnscsi  17563  plendxnbasendx  17573  plendxnplusgndx  17574  plendxnmulrndx  17575  plendxnscandx  17576  plendxnvscandx  17577  dsndxnbasendx  17592  dsndxnplusgndx  17593  dsndxnmulrndx  17594  slotsdnscsi  17595  dsndxntsetndx  17596  unifndxnbasendx  17602  unifndxntsetndx  17603  psgnodpmr  21929  logbrec  27143  2logb9irr  27156  2logb3irr  27158  log2le1  27311  2lgsoddprmlem3a  27770  2lgsoddprmlem3b  27771  2lgsoddprmlem3c  27772  2lgsoddprmlem3d  27773  slotsinbpsd  28936  slotslnbpsd  28937  lngndxnitvndx  28938  konigsberglem2  30887  ex-dif  31057  ex-in  31059  ex-pss  31062  ex-res  31075  dp20u  33517  dp20h  33518  dp2clq  33520  dp2lt10  33523  dp2lt  33524  dplti  33544  dpexpp1  33547  2sqr3nconstr  34496  cos9thpinconstrlem2  34505  ballotlemi1  35218  signswch  35273  itgexpif  35318  hgt750lemd  35360  hgt750lem  35363  fdc  38882  tan3rdpi  43607  asin1half  43612  areaquad  44421  stirlinglem4  47302  stirlinglem13  47311  stirlinglem14  47312  stirlingr  47315  dirker2re  47317  dirkerdenne0  47318  dirkerre  47320  dirkertrigeqlem1  47323  dirkercncflem2  47329  dirkercncflem4  47331  fourierdlem16  47348  fourierdlem21  47353  fourierdlem22  47354  fourierdlem66  47397  fourierdlem83  47414  fourierdlem103  47434  fourierdlem104  47435  sqwvfoura  47453  sqwvfourb  47454  fourierswlem  47455  fouriersw  47456  etransclem46  47505  numtowerdt  48131  goldratval  48151  fmtnoprmfac2lem1  48866  usgrexmpl2nb3  49347  usgrexmpl2nb4  49348  usgrexmpl2nb5  49349  usgrexmpl2trifr  49350  zlmodzxzldeplem  49825  veronesev4lem  51288  veronesev5lem  51289  veronesev6lem  51290  veronesevrowd  51291