Theorem gtneii 11340

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

This proof depends on syntax axioms:   ∈ wcel 2146   ≠ wne 2961   class class class wbr 5114  ℝcr 11117   < clt 11261

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-pre-lttri 11192  ax-pre-lttrn 11193

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-ltxr 11266

This theorem is used by:  ltneii  11341  fztpval  13633  tpf1ofv2  14555  sgnnbi  15167  sgnpbi  15168  geo2sum  15953  bpoly4  16138  ene1  16291  3dvds  16414  3lcm2e6  16816  starvndxnbasendx  17382  starvndxnplusgndx  17383  starvndxnmulrndx  17384  scandxnbasendx  17394  scandxnplusgndx  17395  scandxnmulrndx  17396  vscandxnbasendx  17399  vscandxnplusgndx  17400  vscandxnmulrndx  17401  vscandxnscandx  17402  ipndxnbasendx  17410  ipndxnplusgndx  17411  ipndxnmulrndx  17412  tsetndxnbasendx  17434  tsetndxnplusgndx  17435  tsetndxnmulrndx  17436  tsetndxnstarvndx  17437  slotstnscsi  17438  plendxnbasendx  17448  plendxnplusgndx  17449  plendxnmulrndx  17450  plendxnscandx  17451  plendxnvscandx  17452  dsndxnbasendx  17467  dsndxnplusgndx  17468  dsndxnmulrndx  17469  slotsdnscsi  17470  dsndxntsetndx  17471  unifndxnbasendx  17477  unifndxntsetndx  17478  psgnodpmr  21777  logbrec  26984  2logb9irr  26997  2logb3irr  26999  log2le1  27152  2lgsoddprmlem3a  27611  2lgsoddprmlem3b  27612  2lgsoddprmlem3c  27613  2lgsoddprmlem3d  27614  slotsinbpsd  28747  slotslnbpsd  28748  lngndxnitvndx  28749  konigsberglem2  30641  ex-dif  30811  ex-in  30813  ex-pss  30816  ex-res  30829  dp20u  33234  dp20h  33235  dp2clq  33237  dp2lt10  33240  dp2lt  33241  dplti  33261  dpexpp1  33264  2sqr3nconstr  34202  cos9thpinconstrlem2  34211  ballotlemi1  34925  signswch  34980  itgexpif  35025  hgt750lemd  35067  hgt750lem  35070  fdc  38437  tan3rdpi  43154  asin1half  43159  areaquad  43984  stirlinglem4  46832  stirlinglem13  46841  stirlinglem14  46842  stirlingr  46845  dirker2re  46847  dirkerdenne0  46848  dirkerre  46850  dirkertrigeqlem1  46853  dirkercncflem2  46859  dirkercncflem4  46861  fourierdlem16  46878  fourierdlem21  46883  fourierdlem22  46884  fourierdlem66  46927  fourierdlem83  46944  fourierdlem103  46964  fourierdlem104  46965  sqwvfoura  46983  sqwvfourb  46984  fourierswlem  46985  fouriersw  46986  etransclem46  47035  nthrucw  47648  fmtnoprmfac2lem1  48359  usgrexmpl2nb3  48840  usgrexmpl2nb4  48841  usgrexmpl2nb5  48842  usgrexmpl2trifr  48843  zlmodzxzldeplem  49319