Theorem gtneii 11323

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

Syntax hints:   ∈ wcel 2143   ≠ wne 2958   class class class wbr 5110  ℝcr 11100   < clt 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-pre-lttri 11175  ax-pre-lttrn 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  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 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  ltneii  11324  fztpval  13616  tpf1ofv2  14537  sgnnbi  15143  sgnpbi  15144  geo2sum  15929  bpoly4  16114  ene1  16267  3dvds  16390  3lcm2e6  16792  starvndxnbasendx  17358  starvndxnplusgndx  17359  starvndxnmulrndx  17360  scandxnbasendx  17370  scandxnplusgndx  17371  scandxnmulrndx  17372  vscandxnbasendx  17375  vscandxnplusgndx  17376  vscandxnmulrndx  17377  vscandxnscandx  17378  ipndxnbasendx  17386  ipndxnplusgndx  17387  ipndxnmulrndx  17388  tsetndxnbasendx  17410  tsetndxnplusgndx  17411  tsetndxnmulrndx  17412  tsetndxnstarvndx  17413  slotstnscsi  17414  plendxnbasendx  17424  plendxnplusgndx  17425  plendxnmulrndx  17426  plendxnscandx  17427  plendxnvscandx  17428  dsndxnbasendx  17443  dsndxnplusgndx  17444  dsndxnmulrndx  17445  slotsdnscsi  17446  dsndxntsetndx  17447  unifndxnbasendx  17453  unifndxntsetndx  17454  psgnodpmr  21721  logbrec  26928  2logb9irr  26941  2logb3irr  26943  log2le1  27096  2lgsoddprmlem3a  27555  2lgsoddprmlem3b  27556  2lgsoddprmlem3c  27557  2lgsoddprmlem3d  27558  slotsinbpsd  28691  slotslnbpsd  28692  lngndxnitvndx  28693  konigsberglem2  30585  ex-dif  30755  ex-in  30757  ex-pss  30760  ex-res  30773  dp20u  33178  dp20h  33179  dp2clq  33181  dp2lt10  33184  dp2lt  33185  dplti  33205  dpexpp1  33208  2sqr3nconstr  34152  cos9thpinconstrlem2  34161  ballotlemi1  34874  signswch  34929  itgexpif  34974  hgt750lemd  35016  hgt750lem  35019  fdc  38377  tan3rdpi  43094  asin1half  43099  areaquad  43926  stirlinglem4  46774  stirlinglem13  46783  stirlinglem14  46784  stirlingr  46787  dirker2re  46789  dirkerdenne0  46790  dirkerre  46792  dirkertrigeqlem1  46795  dirkercncflem2  46801  dirkercncflem4  46803  fourierdlem16  46820  fourierdlem21  46825  fourierdlem22  46826  fourierdlem66  46869  fourierdlem83  46886  fourierdlem103  46906  fourierdlem104  46907  sqwvfoura  46925  sqwvfourb  46926  fourierswlem  46927  fouriersw  46928  etransclem46  46977  nthrucw  47590  fmtnoprmfac2lem1  48301  usgrexmpl2nb3  48782  usgrexmpl2nb4  48783  usgrexmpl2nb5  48784  usgrexmpl2trifr  48785  zlmodzxzldeplem  49261