Theorem gtned 11345

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941   class class class wbr 5147  ℝcr 11105   < clt 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  ltned  11346  seqf1olem1  14003  seqf1olem2  14004  hashfun  14393  abssubne0  15259  rpnnen2lem9  16161  rpnnen2lem11  16163  coe1tmmul2  21780  iccpnfcnv  24442  iccpnfhmeo  24443  pmltpclem2  24948  voliunlem1  25049  dvferm1lem  25483  lhop2  25514  ftc1lem5  25539  vieta1lem2  25806  geolim3  25834  logtayl  26150  atanre  26370  lgamgulmlem2  26514  lgamgulmlem3  26515  perfectlem2  26713  axlowdimlem16  28195  clwwisshclwwslem  29247  frgrogt3nreg  29630  qsidomlem1  32529  esumcvgre  33027  eulerpartlems  33297  hgt750lem  33601  ivthALT  35158  unbdqndv2lem2  35324  knoppndvlem17  35342  poimirlem11  36437  poimirlem12  36438  poimirlem24  36450  lcmineqlem11  40842  3lexlogpow2ineq2  40862  aks4d1p1p2  40873  aks4d1p1p4  40874  aks4d1p1p6  40876  aks4d1p1p7  40877  aks4d1p1p5  40878  aks4d1p3  40881  aks4d1p7d1  40885  aks4d1p7  40886  aks4d1p8  40890  aks4d1p9  40891  rtprmirr  41181  sn-0ne2  41223  pellfundne1  41560  eliccelioc  44169  fmul01lt1lem1  44235  lptre2pt  44291  cncfiooicclem1  44544  cncfioobdlem  44547  dvnmul  44594  ditgeqiooicc  44611  itgioocnicc  44628  iblcncfioo  44629  wallispilem4  44719  wallispi  44721  wallispi2lem1  44722  wallispi2lem2  44723  wallispi2  44724  stirlinglem5  44729  fourierdlem4  44762  fourierdlem34  44792  fourierdlem41  44799  fourierdlem42  44800  fourierdlem48  44805  fourierdlem49  44806  fourierdlem61  44818  fourierdlem73  44830  fourierdlem75  44832  fourierdlem76  44833  fourierdlem81  44838  fourierdlem82  44839  fourierdlem84  44841  fourierdlem93  44850  fourierdlem111  44868  fouriersw  44882  etransclem35  44920  qndenserrnbllem  44945  nnfoctbdjlem  45106  hoidmvlelem3  45248  hoiqssbllem2  45274  smfmullem1  45442  sfprmdvdsmersenne  46206  lighneallem2  46209  perfectALTVlem2  46325  eenglngeehlnmlem2  47326