Theorem 1ne2 12395

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 11180	. 2 ⊢ 1 ∈ ℝ
2		1lt2 12358	. 2 ⊢ 1 < 2
3	1, 2	ltneii 11293	1 ⊢ 1 ≠ 2

Syntax hints:   ≠ wne 2926  1c1 11075  2c2 12242

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-2 12250

This theorem is referenced by:  fzprval  13552  fvf1tp  13757  f13idfv  13971  hashprg  14366  elprchashprn2  14367  hash2prde  14441  hash2pwpr  14447  f1oun2prg  14889  geo2sum2  15846  prm2orodd  16667  pmtrprfval  19423  pmtrprfvalrn  19424  zringndrg  21384  m2detleiblem3  22522  m2detleiblem4  22523  m2detleib  22524  ehl2eudis  25328  2logb9irrALT  26714  sqrt2cxp2logb9e3  26715  1sgm2ppw  27117  2lgslem4  27323  2sqlem11  27346  2sqreultlem  27364  2sqreunnltlem  27367  istrkg3ld  28394  axlowdimlem4  28878  axlowdimlem6  28880  umgredgnlp  29080  usgrexmpldifpr  29191  usgrexmplef  29192  konigsbergiedgw  30183  konigsberglem2  30188  ex-hash  30388  cyc3evpm  33113  evl1deg2  33552  evl1deg3  33553  rtelextdg2lem  33722  cos9thpiminplylem3  33780  hgt750lemg  34651  hgt750lemb  34653  tgoldbachgt  34660  aks6d1c7lem1  42163  rabren3dioph  42796  refsum2cnlem1  45024  ovnsubadd2lem  46636  oddprmALTV  47678  nnsum3primes4  47779  nnsum3primesgbe  47783  nnsum4primesodd  47787  nnsum4primesoddALTV  47788  usgrexmpl1lem  48002  usgrexmpl2lem  48007  usgrexmpl2nb1  48013  usgrexmpl2nb2  48014  usgrexmpl2trifr  48018  nnlog2ge0lt1  48545  logbpw2m1  48546  fllog2  48547  blennnelnn  48555  nnpw2blen  48559  blen1  48563  blen2  48564  blen1b  48567  blennnt2  48568  nnolog2flm1  48569  blennngt2o2  48571  blennn0e2  48573  fv1prop  48678  fv2prop  48679  prelrrx2  48692  prelrrx2b  48693  rrx2xpref1o  48697  rrx2plordisom  48702  ehl2eudisval0  48704  line2ylem  48730  line2  48731  line2x  48733  line2y  48734  itscnhlinecirc02p  48764  inlinecirc02plem  48765