Theorem 1ne2 12553

Description: 1 is not equal to 2. (Contributed by NM, 19-Oct-2012.)

Assertion

Ref	Expression
1ne2	⊢ 1 ≠ 2

Proof of Theorem 1ne2

Step	Hyp	Ref	Expression
1		1re 11308	. 2 ⊢ 1 ∈ ℝ
2		1lt2 12515	. 2 ⊢ 1 < 2
3	1, 2	ltneii 11423	1 ⊢ 1 ≠ 2

This proof depends on syntax axioms:   ≠ wne 2956  1c1 11201  2c2 12397

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-2 12405

This theorem is used by:  fzprval  13719  fvf1tp  13929  f13idfv  14143  hashprg  14539  elprchashprn2  14540  hash2prde  14615  hash2pwpr  14621  f1oun2prg  15068  geo2sum2  16043  prm2orodd  16866  pmtrprfval  19701  pmtrprfvalrn  19702  zringndrg  21774  m2detleiblem3  22944  m2detleiblem4  22945  m2detleib  22946  ehl2eudis  25743  2logb9irrALT  27126  sqrt2cxp2logb9e3  27127  1sgm2ppw  27527  2lgslem4  27733  2sqlem11  27756  2sqreultlem  27774  2sqreunnltlem  27777  flt0  27969  istrkg3ld  28923  axlowdimlem4  29523  axlowdimlem6  29525  umgredgnlp  29725  usgrexmpldifpr  29839  usgrexmplef  29840  konigsbergiedgw  30849  konigsberglem2  30854  ex-hash  31054  cyc3evpm  33711  evl1deg2  34109  evl1deg3  34110  rtelextdg2lem  34358  cos9thpiminplylem3  34416  hgt750lemg  35283  hgt750lemb  35285  tgoldbachgt  35292  aks6d1c7lem1  43230  rabren3dioph  43821  refsum2cnlem1  46053  ovnsubadd2lem  47654  oddprmALTV  48784  nnsum3primes4  48885  nnsum3primesgbe  48889  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb1  49129  usgrexmpl2nb2  49130  usgrexmpl2trifr  49134  gpg5edgnedg  49227  nnlog2ge0lt1  49677  logbpw2m1  49678  fllog2  49679  blennnelnn  49687  nnpw2blen  49691  blen1  49695  blen2  49696  blen1b  49699  blennnt2  49700  nnolog2flm1  49701  blennngt2o2  49703  blennn0e2  49705  fv1prop  49810  fv2prop  49811  prelrrx2  49824  prelrrx2b  49825  rrx2xpref1o  49829  rrx2plordisom  49834  ehl2eudisval0  49836  line2ylem  49862  line2  49863  line2x  49865  line2y  49866  itscnhlinecirc02p  49896  inlinecirc02plem  49897  crosspv2d  50960  crosspdotsumlem  50963  veronesev1lem  50972  veronesev2lem  50973  veronesevrowd  50978