Theorem gtneii 10944

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

Syntax hints:   ∈ wcel 2110   ≠ wne 2940   class class class wbr 5053  ℝcr 10728   < clt 10867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-resscn 10786  ax-pre-lttri 10803  ax-pre-lttrn 10804

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-po 5468  df-so 5469  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-ltxr 10872

This theorem is referenced by:  ltneii  10945  fztpval  13174  geo2sum  15437  bpoly4  15621  ene1  15771  3dvds  15892  3lcm2e6  16288  resslemOLD  16794  starvndxnbasendx  16847  scandxnbasendx  16857  vscandxnbasendx  16860  ipndxnbasendx  16868  tsetndxnbasendx  16887  plendxnbasendx  16895  dsndxnbasendx  16905  unifndxnbasendx  16908  resccoOLD  17338  oppgtset  18744  symgvalstruct  18789  mgpsca  19511  mgptset  19512  mgpds  19514  cnfldfun  20375  psgnodpmr  20552  matsca  21312  matvsca  21313  tuslem  23164  setsmsds  23374  tngds  23546  logbrec  25665  2logb9irr  25678  2logb3irr  25680  log2le1  25833  2lgsoddprmlem3a  26291  2lgsoddprmlem3b  26292  2lgsoddprmlem3c  26293  2lgsoddprmlem3d  26294  konigsberglem2  28336  ex-dif  28506  ex-in  28508  ex-pss  28511  ex-res  28524  dp20u  30872  dp20h  30873  dp2clq  30875  dp2lt10  30878  dp2lt  30879  dplti  30899  dpexpp1  30902  oppgle  30958  resvvsca  31252  zlmds  31626  zlmtset  31627  ballotlemi1  32181  sgnnbi  32224  sgnpbi  32225  signswch  32252  itgexpif  32298  hgt750lemd  32340  hgt750lem  32343  fdc  35640  areaquad  40750  mnringscad  41515  mnringvscad  41516  stirlinglem4  43293  stirlinglem13  43302  stirlinglem14  43303  stirlingr  43306  dirker2re  43308  dirkerdenne0  43309  dirkerre  43311  dirkertrigeqlem1  43314  dirkercncflem2  43320  dirkercncflem4  43322  fourierdlem16  43339  fourierdlem21  43344  fourierdlem22  43345  fourierdlem66  43388  fourierdlem83  43405  fourierdlem103  43425  fourierdlem104  43426  sqwvfoura  43444  sqwvfourb  43445  fourierswlem  43446  fouriersw  43447  etransclem46  43496  fmtnoprmfac2lem1  44691  zlmodzxzldeplem  45512