Theorem gtned 11272

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 11234	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5086  ℝcr 11028   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  ltned  11273  gt0ne0d  11705  fzdif1  13550  seqf1olem1  13994  seqf1olem2  13995  hashfun  14390  abssubne0  15270  rpnnen2lem9  16180  rpnnen2lem11  16182  coe1tmmul2  22251  iccpnfcnv  24921  iccpnfhmeo  24922  pmltpclem2  25426  voliunlem1  25527  dvferm1lem  25961  lhop2  25992  ftc1lem5  26017  vieta1lem2  26288  geolim3  26316  logtayl  26637  rtprmirr  26737  atanre  26862  lgamgulmlem2  27007  lgamgulmlem3  27008  perfectlem2  27207  axlowdimlem16  29040  clwwisshclwwslem  30099  frgrogt3nreg  30482  qsidomlem1  33527  madjusmdetlem2  33988  esumcvgre  34251  eulerpartlems  34520  hgt750lem  34811  ivthALT  36533  unbdqndv2lem2  36786  knoppndvlem17  36804  poimirlem11  37966  poimirlem12  37967  poimirlem24  37979  lcmineqlem11  42492  3lexlogpow2ineq2  42512  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p3  42531  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  aks6d1c1  42569  aks6d1c7lem1  42633  aks6d1c7lem2  42634  sn-0ne2  42852  pellfundne1  43335  eliccelioc  45969  fmul01lt1lem1  46032  lptre2pt  46086  cncfiooicclem1  46339  cncfioobdlem  46342  dvnmul  46389  ditgeqiooicc  46406  itgioocnicc  46423  iblcncfioo  46424  wallispilem4  46514  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem5  46524  fourierdlem4  46557  fourierdlem34  46587  fourierdlem41  46594  fourierdlem42  46595  fourierdlem48  46600  fourierdlem49  46601  fourierdlem61  46613  fourierdlem73  46625  fourierdlem75  46627  fourierdlem76  46628  fourierdlem81  46633  fourierdlem82  46634  fourierdlem84  46636  fourierdlem93  46645  fourierdlem111  46663  fouriersw  46677  etransclem35  46715  qndenserrnbllem  46740  nnfoctbdjlem  46901  hoidmvlelem3  47043  hoiqssbllem2  47069  smfmullem1  47237  sfprmdvdsmersenne  48078  lighneallem2  48081  perfectALTVlem2  48210  eenglngeehlnmlem2  49226