Theorem gtned 11333

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

Syntax hints:   → wi 4   ∈ wcel 2145   ≠ wne 2960   class class class wbr 5105  ℝcr 11087   < clt 11231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-resscn 11145  ax-pre-lttri 11162  ax-pre-lttrn 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-po 5560  df-so 5561  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236

This theorem is referenced by:  ltned  11334  gt0ne0d  11766  fzdif1  13624  seqf1olem1  14068  seqf1olem2  14069  hashfun  14464  abssubne0  15358  rpnnen2lem9  16268  rpnnen2lem11  16270  qsidomlem1  21440  coe1tmmul2  22397  iccpnfcnv  25064  iccpnfhmeo  25065  pmltpclem2  25569  voliunlem1  25670  dvferm1lem  26104  lhop2  26135  ftc1lem5  26160  vieta1lem2  26433  geolim3  26461  logtayl  26783  rtprmirr  26883  atanre  27008  lgamgulmlem2  27152  lgamgulmlem3  27153  perfectlem2  27352  axlowdimlem16  29216  clwwisshclwwslem  30274  frgrogt3nreg  30657  madjusmdetlem2  34135  esumcvgre  34398  eulerpartlems  34667  hgt750lem  34955  ivthALT  36708  unbdqndv2lem2  36961  knoppndvlem17  36979  poimirlem11  38142  poimirlem12  38143  poimirlem24  38155  lcmineqlem11  42668  3lexlogpow2ineq2  42688  aks4d1p1p2  42699  aks4d1p1p4  42700  aks4d1p1p6  42702  aks4d1p1p7  42703  aks4d1p1p5  42704  aks4d1p3  42707  aks4d1p7d1  42711  aks4d1p7  42712  aks4d1p8  42716  aks4d1p9  42717  aks6d1c1  42745  aks6d1c7lem1  42809  aks6d1c7lem2  42810  sn-0ne2  43027  pellfundne1  43478  eliccelioc  46095  fmul01lt1lem1  46158  lptre2pt  46212  cncfiooicclem1  46465  cncfioobdlem  46468  dvnmul  46515  ditgeqiooicc  46532  itgioocnicc  46549  iblcncfioo  46550  wallispilem4  46640  wallispi  46642  wallispi2lem1  46643  wallispi2lem2  46644  wallispi2  46645  stirlinglem5  46650  fourierdlem4  46683  fourierdlem34  46713  fourierdlem41  46720  fourierdlem42  46721  fourierdlem48  46726  fourierdlem49  46727  fourierdlem61  46739  fourierdlem73  46751  fourierdlem75  46753  fourierdlem76  46754  fourierdlem81  46759  fourierdlem82  46760  fourierdlem84  46762  fourierdlem93  46771  fourierdlem111  46789  fouriersw  46803  etransclem35  46841  qndenserrnbllem  46866  nnfoctbdjlem  47027  hoidmvlelem3  47169  hoiqssbllem2  47195  smfmullem1  47363  sfprmdvdsmersenne  48210  lighneallem2  48213  perfectALTVlem2  48342  eenglngeehlnmlem2  49369