Theorem 1ne2 11848

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 10643	. 2 ⊢ 1 ∈ ℝ
2		1lt2 11811	. 2 ⊢ 1 < 2
3	1, 2	ltneii 10755	1 ⊢ 1 ≠ 2

Syntax hints:   ≠ wne 3018  1c1 10540  2c2 11695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-2 11703

This theorem is referenced by:  fzprval  12971  f13idfv  13371  hashprg  13759  elprchashprn2  13760  hash2prde  13831  hash2pwpr  13837  f1oun2prg  14281  geo2sum2  15232  prm2orodd  16037  basendxnplusgndx  16610  oppgbas  18481  pmtrprfval  18617  pmtrprfvalrn  18618  mgpbas  19247  mgpress  19252  zringndrg  20639  m2detleiblem3  21240  m2detleiblem4  21241  m2detleib  21242  ehl2eudis  24027  2logb9irrALT  25378  sqrt2cxp2logb9e3  25379  1sgm2ppw  25778  2lgslem4  25984  2sqlem11  26007  2sqreultlem  26025  2sqreunnltlem  26028  istrkg3ld  26249  axlowdimlem4  26733  axlowdimlem6  26735  umgredgnlp  26934  usgrexmpldifpr  27042  usgrexmplef  27043  konigsbergiedgw  28029  konigsberglem2  28034  ex-hash  28234  cyc3evpm  30794  hgt750lemg  31927  hgt750lemb  31929  tgoldbachgt  31936  rabren3dioph  39419  refsum2cnlem1  41301  ovnsubadd2lem  42934  oddprmALTV  43859  nnsum3primes4  43960  nnsum3primesgbe  43964  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  nnlog2ge0lt1  44633  logbpw2m1  44634  fllog2  44635  blennnelnn  44643  nnpw2blen  44647  blen1  44651  blen2  44652  blen1b  44655  blennnt2  44656  nnolog2flm1  44657  blennngt2o2  44659  blennn0e2  44661  fv1prop  44693  fv2prop  44694  prelrrx2  44707  prelrrx2b  44708  rrx2xpref1o  44712  rrx2plordisom  44717  ehl2eudisval0  44719  line2ylem  44745  line2  44746  line2x  44748  line2y  44749  itscnhlinecirc02p  44779  inlinecirc02plem  44780