Theorem 1ne2 11655

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 10439	. 2 ⊢ 1 ∈ ℝ
2		1lt2 11618	. 2 ⊢ 1 < 2
3	1, 2	ltneii 10553	1 ⊢ 1 ≠ 2

Syntax hints:   ≠ wne 2968  1c1 10336  2c2 11495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-po 5326  df-so 5327  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-2 11503

This theorem is referenced by:  fzprval  12784  f13idfv  13183  hashprg  13569  elprchashprn2  13570  hash2prde  13639  hash2pwpr  13645  f1oun2prg  14141  geo2sum2  15090  prm2orodd  15891  basendxnplusgndx  16464  oppgbas  18250  pmtrprfval  18376  pmtrprfvalrn  18377  mgpbas  18968  mgpress  18973  zringndrg  20339  m2detleiblem3  20942  m2detleiblem4  20943  m2detleib  20944  ehl2eudis  23728  2logb9irrALT  25077  sqrt2cxp2logb9e3  25078  1sgm2ppw  25478  2lgslem4  25684  2sqlem11  25707  2sqreultlem  25725  2sqreunnltlem  25728  istrkg3ld  25949  axlowdimlem4  26434  axlowdimlem6  26436  umgredgnlp  26635  usgrexmpldifpr  26743  usgrexmplef  26744  konigsbergiedgw  27780  konigsberglem2  27785  ex-hash  28010  hgt750lemg  31570  hgt750lemb  31572  tgoldbachgt  31579  rabren3dioph  38805  refsum2cnlem1  40710  ovnsubadd2lem  42356  oddprmALTV  43218  nnsum3primes4  43319  nnsum3primesgbe  43323  nnsum4primesodd  43327  nnsum4primesoddALTV  43328  nnlog2ge0lt1  43992  logbpw2m1  43993  fllog2  43994  blennnelnn  44002  nnpw2blen  44006  blen1  44010  blen2  44011  blen1b  44014  blennnt2  44015  nnolog2flm1  44016  blennngt2o2  44018  blennn0e2  44020  fv1prop  44052  fv2prop  44053  prelrrx2  44066  prelrrx2b  44067  rrx2xpref1o  44071  rrx2plordisom  44076  ehl2eudisval0  44078  line2ylem  44104  line2  44105  line2x  44107  line2y  44108  itscnhlinecirc02p  44138  inlinecirc02plem  44139