Theorem gtned 11370

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2932   class class class wbr 5119  ℝcr 11128   < clt 11269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-pre-lttri 11203  ax-pre-lttrn 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-ltxr 11274

This theorem is referenced by:  ltned  11371  fzdif1  13622  seqf1olem1  14059  seqf1olem2  14060  hashfun  14455  abssubne0  15335  rpnnen2lem9  16240  rpnnen2lem11  16242  coe1tmmul2  22213  iccpnfcnv  24893  iccpnfhmeo  24894  pmltpclem2  25402  voliunlem1  25503  dvferm1lem  25940  lhop2  25972  ftc1lem5  25999  vieta1lem2  26271  geolim3  26299  logtayl  26621  rtprmirr  26722  atanre  26847  lgamgulmlem2  26992  lgamgulmlem3  26993  perfectlem2  27193  axlowdimlem16  28936  clwwisshclwwslem  29995  frgrogt3nreg  30378  qsidomlem1  33467  madjusmdetlem2  33859  esumcvgre  34122  eulerpartlems  34392  hgt750lem  34683  ivthALT  36353  unbdqndv2lem2  36528  knoppndvlem17  36546  poimirlem11  37655  poimirlem12  37656  poimirlem24  37668  lcmineqlem11  42052  3lexlogpow2ineq2  42072  aks4d1p1p2  42083  aks4d1p1p4  42084  aks4d1p1p6  42086  aks4d1p1p7  42087  aks4d1p1p5  42088  aks4d1p3  42091  aks4d1p7d1  42095  aks4d1p7  42096  aks4d1p8  42100  aks4d1p9  42101  aks6d1c1  42129  aks6d1c7lem1  42193  aks6d1c7lem2  42194  sn-0ne2  42449  pellfundne1  42912  eliccelioc  45550  fmul01lt1lem1  45613  lptre2pt  45669  cncfiooicclem1  45922  cncfioobdlem  45925  dvnmul  45972  ditgeqiooicc  45989  itgioocnicc  46006  iblcncfioo  46007  wallispilem4  46097  wallispi  46099  wallispi2lem1  46100  wallispi2lem2  46101  wallispi2  46102  stirlinglem5  46107  fourierdlem4  46140  fourierdlem34  46170  fourierdlem41  46177  fourierdlem42  46178  fourierdlem48  46183  fourierdlem49  46184  fourierdlem61  46196  fourierdlem73  46208  fourierdlem75  46210  fourierdlem76  46211  fourierdlem81  46216  fourierdlem82  46217  fourierdlem84  46219  fourierdlem93  46228  fourierdlem111  46246  fouriersw  46260  etransclem35  46298  qndenserrnbllem  46323  nnfoctbdjlem  46484  hoidmvlelem3  46626  hoiqssbllem2  46652  smfmullem1  46820  sfprmdvdsmersenne  47617  lighneallem2  47620  perfectALTVlem2  47736  eenglngeehlnmlem2  48718