Theorem gtned 11245

Description: 'Less than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltned.2	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
gtned	⊢ (𝜑 → 𝐵 ≠ 𝐴)

Proof of Theorem gtned

Step	Hyp	Ref	Expression
1		ltd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltned.2	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
3		ltne 11207	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928   class class class wbr 5091  ℝcr 11002   < clt 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11060  ax-pre-lttri 11077  ax-pre-lttrn 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11145  df-mnf 11146  df-ltxr 11148

This theorem is referenced by:  ltned  11246  gt0ne0d  11678  fzdif1  13502  seqf1olem1  13945  seqf1olem2  13946  hashfun  14341  abssubne0  15221  rpnnen2lem9  16128  rpnnen2lem11  16130  coe1tmmul2  22188  iccpnfcnv  24867  iccpnfhmeo  24868  pmltpclem2  25375  voliunlem1  25476  dvferm1lem  25913  lhop2  25945  ftc1lem5  25972  vieta1lem2  26244  geolim3  26272  logtayl  26594  rtprmirr  26695  atanre  26820  lgamgulmlem2  26965  lgamgulmlem3  26966  perfectlem2  27166  axlowdimlem16  28933  clwwisshclwwslem  29989  frgrogt3nreg  30372  qsidomlem1  33412  madjusmdetlem2  33836  esumcvgre  34099  eulerpartlems  34368  hgt750lem  34659  ivthALT  36368  unbdqndv2lem2  36543  knoppndvlem17  36561  poimirlem11  37670  poimirlem12  37671  poimirlem24  37683  lcmineqlem11  42071  3lexlogpow2ineq2  42091  aks4d1p1p2  42102  aks4d1p1p4  42103  aks4d1p1p6  42105  aks4d1p1p7  42106  aks4d1p1p5  42107  aks4d1p3  42110  aks4d1p7d1  42114  aks4d1p7  42115  aks4d1p8  42119  aks4d1p9  42120  aks6d1c1  42148  aks6d1c7lem1  42212  aks6d1c7lem2  42213  sn-0ne2  42438  pellfundne1  42921  eliccelioc  45560  fmul01lt1lem1  45623  lptre2pt  45677  cncfiooicclem1  45930  cncfioobdlem  45933  dvnmul  45980  ditgeqiooicc  45997  itgioocnicc  46014  iblcncfioo  46015  wallispilem4  46105  wallispi  46107  wallispi2lem1  46108  wallispi2lem2  46109  wallispi2  46110  stirlinglem5  46115  fourierdlem4  46148  fourierdlem34  46178  fourierdlem41  46185  fourierdlem42  46186  fourierdlem48  46191  fourierdlem49  46192  fourierdlem61  46204  fourierdlem73  46216  fourierdlem75  46218  fourierdlem76  46219  fourierdlem81  46224  fourierdlem82  46225  fourierdlem84  46227  fourierdlem93  46236  fourierdlem111  46254  fouriersw  46268  etransclem35  46306  qndenserrnbllem  46331  nnfoctbdjlem  46492  hoidmvlelem3  46634  hoiqssbllem2  46660  smfmullem1  46828  sfprmdvdsmersenne  47633  lighneallem2  47636  perfectALTVlem2  47752  eenglngeehlnmlem2  48769