Theorem gtned 11280

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5100  ℝcr 11037   < clt 11178

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183

This theorem is referenced by:  ltned  11281  gt0ne0d  11713  fzdif1  13533  seqf1olem1  13976  seqf1olem2  13977  hashfun  14372  abssubne0  15252  rpnnen2lem9  16159  rpnnen2lem11  16161  coe1tmmul2  22230  iccpnfcnv  24910  iccpnfhmeo  24911  pmltpclem2  25418  voliunlem1  25519  dvferm1lem  25956  lhop2  25988  ftc1lem5  26015  vieta1lem2  26287  geolim3  26315  logtayl  26637  rtprmirr  26738  atanre  26863  lgamgulmlem2  27008  lgamgulmlem3  27009  perfectlem2  27209  axlowdimlem16  29042  clwwisshclwwslem  30101  frgrogt3nreg  30484  qsidomlem1  33544  madjusmdetlem2  34005  esumcvgre  34268  eulerpartlems  34537  hgt750lem  34828  ivthALT  36548  unbdqndv2lem2  36729  knoppndvlem17  36747  poimirlem11  37876  poimirlem12  37877  poimirlem24  37889  lcmineqlem11  42403  3lexlogpow2ineq2  42423  aks4d1p1p2  42434  aks4d1p1p4  42435  aks4d1p1p6  42437  aks4d1p1p7  42438  aks4d1p1p5  42439  aks4d1p3  42442  aks4d1p7d1  42446  aks4d1p7  42447  aks4d1p8  42451  aks4d1p9  42452  aks6d1c1  42480  aks6d1c7lem1  42544  aks6d1c7lem2  42545  sn-0ne2  42770  pellfundne1  43240  eliccelioc  45875  fmul01lt1lem1  45938  lptre2pt  45992  cncfiooicclem1  46245  cncfioobdlem  46248  dvnmul  46295  ditgeqiooicc  46312  itgioocnicc  46329  iblcncfioo  46330  wallispilem4  46420  wallispi  46422  wallispi2lem1  46423  wallispi2lem2  46424  wallispi2  46425  stirlinglem5  46430  fourierdlem4  46463  fourierdlem34  46493  fourierdlem41  46500  fourierdlem42  46501  fourierdlem48  46506  fourierdlem49  46507  fourierdlem61  46519  fourierdlem73  46531  fourierdlem75  46533  fourierdlem76  46534  fourierdlem81  46539  fourierdlem82  46540  fourierdlem84  46542  fourierdlem93  46551  fourierdlem111  46569  fouriersw  46583  etransclem35  46621  qndenserrnbllem  46646  nnfoctbdjlem  46807  hoidmvlelem3  46949  hoiqssbllem2  46975  smfmullem1  47143  sfprmdvdsmersenne  47957  lighneallem2  47960  perfectALTVlem2  48076  eenglngeehlnmlem2  49092