Theorem 3ne0 12281

Description: The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Assertion

Ref	Expression
3ne0	⊢ 3 ≠ 0

Proof of Theorem 3ne0

Step	Hyp	Ref	Expression
1		3nn 12254	. 2 ⊢ 3 ∈ ℕ
2	1	nnne0i 12211	1 ⊢ 3 ≠ 0

Syntax hints:   ≠ wne 2933  0cc0 11032  3c3 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-2 12238  df-3 12239

This theorem is referenced by:  8th4div3  12391  halfthird  12392  halfpm6th  12393  f1oun2prg  14873  01sqrexlem7  15204  caurcvgr  15630  bpoly2  16016  bpoly3  16017  bpoly4  16018  sin01bnd  16146  cos01bnd  16147  cos1bnd  16148  cos2bnd  16149  sin01gt0  16151  cos01gt0  16152  rpnnen2lem3  16177  rpnnen2lem11  16185  tangtx  26485  sincos6thpi  26496  sincos3rdpi  26497  pigt3  26498  pige3ALT  26500  2logb9irrALT  26778  1cubr  26822  dcubic1lem  26823  dcubic2  26824  dcubic1  26825  dcubic  26826  mcubic  26827  cubic2  26828  cubic  26829  quartlem3  26839  log2cnv  26924  log2tlbnd  26925  ppiub  27184  bclbnd  27260  bposlem6  27269  bposlem9  27272  usgrexmplef  29345  upgr4cycl4dv4e  30273  konigsbergiedgw  30336  konigsberglem1  30340  konigsberglem3  30342  konigsberglem5  30344  ex-lcm  30546  ply1dg3rt0irred  33662  iconstr  33929  2sqr3minply  33943  2sqr3nconstr  33944  cos9thpiminplylem3  33947  cos9thpiminplylem4  33948  cos9thpiminplylem5  33949  cos9thpiminply  33951  cos9thpinconstrlem1  33952  cos9thpinconstrlem2  33953  cos9thpinconstr  33954  hgt750lem  34814  cusgracyclt3v  35357  sinccvglem  35873  mblfinlem3  37997  itg2addnclem2  38010  itg2addnclem3  38011  3rdpwhole  42741  tan3rdpi  42801  sin2t3rdpi  42802  cos2t3rdpi  42803  sin4t3rdpi  42804  cos4t3rdpi  42805  acos1half  42807  3cubeslem2  43134  lhe4.4ex1a  44777  stoweidlem11  46460  stoweidlem13  46462  stoweidlem26  46475  stoweidlem34  46483  stoweidlem42  46491  stoweidlem59  46508  stoweidlem62  46511  stoweid  46512  wallispilem4  46517  wallispi2lem1  46520  stirlinglem11  46533  fourierdlem87  46642  usgrexmpl2lem  48517  usgrexmpl2nb3  48525  usgrexmpl2trifr  48528  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem4  48610  itcoval3  49156  sepfsepc  49418