Theorem 1ne2 12428

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 11181	. 2 ⊢ 1 ∈ ℝ
2		1lt2 12390	. 2 ⊢ 1 < 2
3	1, 2	ltneii 11296	1 ⊢ 1 ≠ 2

Syntax hints:   ≠ wne 2957  1c1 11074  2c2 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-2 12280

This theorem is referenced by:  fzprval  13590  fvf1tp  13799  f13idfv  14013  hashprg  14408  elprchashprn2  14409  hash2prde  14483  hash2pwpr  14489  f1oun2prg  14930  geo2sum2  15904  prm2orodd  16725  pmtrprfval  19527  pmtrprfvalrn  19528  zringndrg  21517  m2detleiblem3  22686  m2detleiblem4  22687  m2detleib  22688  ehl2eudis  25481  2logb9irrALT  26860  sqrt2cxp2logb9e3  26861  1sgm2ppw  27261  2lgslem4  27467  2sqlem11  27490  2sqreultlem  27508  2sqreunnltlem  27511  istrkg3ld  28627  axlowdimlem4  29143  axlowdimlem6  29145  umgredgnlp  29345  usgrexmpldifpr  29456  usgrexmplef  29457  konigsbergiedgw  30447  konigsberglem2  30452  ex-hash  30652  cyc3evpm  33327  evl1deg2  33770  evl1deg3  33771  rtelextdg2lem  34020  cos9thpiminplylem3  34078  hgt750lemg  34945  hgt750lemb  34947  tgoldbachgt  34954  aks6d1c7lem1  42794  rabren3dioph  43389  refsum2cnlem1  45614  ovnsubadd2lem  47216  oddprmALTV  48306  nnsum3primes4  48407  nnsum3primesgbe  48411  nnsum4primesodd  48415  nnsum4primesoddALTV  48416  usgrexmpl1lem  48640  usgrexmpl2lem  48645  usgrexmpl2nb1  48651  usgrexmpl2nb2  48652  usgrexmpl2trifr  48656  gpg5edgnedg  48749  nnlog2ge0lt1  49185  logbpw2m1  49186  fllog2  49187  blennnelnn  49195  nnpw2blen  49199  blen1  49203  blen2  49204  blen1b  49207  blennnt2  49208  nnolog2flm1  49209  blennngt2o2  49211  blennn0e2  49213  fv1prop  49318  fv2prop  49319  prelrrx2  49332  prelrrx2b  49333  rrx2xpref1o  49337  rrx2plordisom  49342  ehl2eudisval0  49344  line2ylem  49370  line2  49371  line2x  49373  line2y  49374  itscnhlinecirc02p  49404  inlinecirc02plem  49405