Theorem gtneii 11425

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

This proof depends on syntax axioms:   ∈ wcel 2144   ≠ wne 2955   class class class wbr 5102  ℝcr 11202   < clt 11346

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11260  ax-pre-lttri 11277  ax-pre-lttrn 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-ltxr 11351

This theorem is used by:  ltneii  11426  fztpval  13723  tpf1ofv2  14646  sgnnbi  15262  sgnpbi  15263  geo2sum  16047  bpoly4  16230  ene1  16383  3dvds  16506  3lcm2e6  16913  starvndxnbasendx  17480  starvndxnplusgndx  17481  starvndxnmulrndx  17482  scandxnbasendx  17492  scandxnplusgndx  17493  scandxnmulrndx  17494  vscandxnbasendx  17497  vscandxnplusgndx  17498  vscandxnmulrndx  17499  vscandxnscandx  17500  ipndxnbasendx  17508  ipndxnplusgndx  17509  ipndxnmulrndx  17510  tsetndxnbasendx  17532  tsetndxnplusgndx  17533  tsetndxnmulrndx  17534  tsetndxnstarvndx  17535  slotstnscsi  17536  plendxnbasendx  17546  plendxnplusgndx  17547  plendxnmulrndx  17548  plendxnscandx  17549  plendxnvscandx  17550  dsndxnbasendx  17565  dsndxnplusgndx  17566  dsndxnmulrndx  17567  slotsdnscsi  17568  dsndxntsetndx  17569  unifndxnbasendx  17575  unifndxntsetndx  17576  psgnodpmr  21901  logbrec  27115  2logb9irr  27128  2logb3irr  27130  log2le1  27283  2lgsoddprmlem3a  27742  2lgsoddprmlem3b  27743  2lgsoddprmlem3c  27744  2lgsoddprmlem3d  27745  slotsinbpsd  28908  slotslnbpsd  28909  lngndxnitvndx  28910  konigsberglem2  30859  ex-dif  31029  ex-in  31031  ex-pss  31034  ex-res  31047  dp20u  33490  dp20h  33491  dp2clq  33493  dp2lt10  33496  dp2lt  33497  dplti  33517  dpexpp1  33520  2sqr3nconstr  34459  cos9thpinconstrlem2  34468  ballotlemi1  35181  signswch  35236  itgexpif  35281  hgt750lemd  35323  hgt750lem  35326  fdc  38772  tan3rdpi  43496  asin1half  43501  areaquad  44311  stirlinglem4  47180  stirlinglem13  47189  stirlinglem14  47190  stirlingr  47193  dirker2re  47195  dirkerdenne0  47196  dirkerre  47198  dirkertrigeqlem1  47201  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem16  47226  fourierdlem21  47231  fourierdlem22  47232  fourierdlem66  47275  fourierdlem83  47292  fourierdlem103  47312  fourierdlem104  47313  sqwvfoura  47331  sqwvfourb  47332  fourierswlem  47333  fouriersw  47334  etransclem46  47383  numtowerdt  48009  goldratval  48029  fmtnoprmfac2lem1  48744  usgrexmpl2nb3  49225  usgrexmpl2nb4  49226  usgrexmpl2nb5  49227  usgrexmpl2trifr  49228  zlmodzxzldeplem  49703  veronesev4lem  51144  veronesev5lem  51145  veronesev6lem  51146  veronesevrowd  51147