Theorem gtned 11299

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

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2939   class class class wbr 5110  ℝcr 11059   < clt 11198

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-pre-lttri 11134  ax-pre-lttrn 11135

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-ltxr 11203

This theorem is referenced by:  ltned  11300  seqf1olem1  13957  seqf1olem2  13958  hashfun  14347  abssubne0  15213  rpnnen2lem9  16115  rpnnen2lem11  16117  coe1tmmul2  21684  iccpnfcnv  24344  iccpnfhmeo  24345  pmltpclem2  24850  voliunlem1  24951  dvferm1lem  25385  lhop2  25416  ftc1lem5  25441  vieta1lem2  25708  geolim3  25736  logtayl  26052  atanre  26272  lgamgulmlem2  26416  lgamgulmlem3  26417  perfectlem2  26615  axlowdimlem16  27969  clwwisshclwwslem  29021  frgrogt3nreg  29404  qsidomlem1  32301  esumcvgre  32779  eulerpartlems  33049  hgt750lem  33353  ivthALT  34883  unbdqndv2lem2  35049  knoppndvlem17  35067  poimirlem11  36162  poimirlem12  36163  poimirlem24  36175  lcmineqlem11  40569  3lexlogpow2ineq2  40589  aks4d1p1p2  40600  aks4d1p1p4  40601  aks4d1p1p6  40603  aks4d1p1p7  40604  aks4d1p1p5  40605  aks4d1p3  40608  aks4d1p7d1  40612  aks4d1p7  40613  aks4d1p8  40617  aks4d1p9  40618  rtprmirr  40891  sn-0ne2  40933  pellfundne1  41270  eliccelioc  43879  fmul01lt1lem1  43945  lptre2pt  44001  cncfiooicclem1  44254  cncfioobdlem  44257  dvnmul  44304  ditgeqiooicc  44321  itgioocnicc  44338  iblcncfioo  44339  wallispilem4  44429  wallispi  44431  wallispi2lem1  44432  wallispi2lem2  44433  wallispi2  44434  stirlinglem5  44439  fourierdlem4  44472  fourierdlem34  44502  fourierdlem41  44509  fourierdlem42  44510  fourierdlem48  44515  fourierdlem49  44516  fourierdlem61  44528  fourierdlem73  44540  fourierdlem75  44542  fourierdlem76  44543  fourierdlem81  44548  fourierdlem82  44549  fourierdlem84  44551  fourierdlem93  44560  fourierdlem111  44578  fouriersw  44592  etransclem35  44630  qndenserrnbllem  44655  nnfoctbdjlem  44816  hoidmvlelem3  44958  hoiqssbllem2  44984  smfmullem1  45152  sfprmdvdsmersenne  45915  lighneallem2  45918  perfectALTVlem2  46034  eenglngeehlnmlem2  46944