Theorem 3ne0 12251

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 12224	. 2 ⊢ 3 ∈ ℕ
2	1	nnne0i 12185	1 ⊢ 3 ≠ 0

Syntax hints:   ≠ wne 2932  0cc0 11026  3c3 12201

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-2 12208  df-3 12209

This theorem is referenced by:  8th4div3  12361  halfthird  12362  halfpm6th  12363  f1oun2prg  14840  01sqrexlem7  15171  caurcvgr  15597  bpoly2  15980  bpoly3  15981  bpoly4  15982  sin01bnd  16110  cos01bnd  16111  cos1bnd  16112  cos2bnd  16113  sin01gt0  16115  cos01gt0  16116  rpnnen2lem3  16141  rpnnen2lem11  16149  tangtx  26470  sincos6thpi  26481  sincos3rdpi  26482  pigt3  26483  pige3ALT  26485  2logb9irrALT  26764  1cubr  26808  dcubic1lem  26809  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  quartlem3  26825  log2cnv  26910  log2tlbnd  26911  ppiub  27171  bclbnd  27247  bposlem6  27256  bposlem9  27259  usgrexmplef  29332  upgr4cycl4dv4e  30260  konigsbergiedgw  30323  konigsberglem1  30327  konigsberglem3  30329  konigsberglem5  30331  ex-lcm  30533  ply1dg3rt0irred  33665  iconstr  33923  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpiminplylem3  33941  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cos9thpinconstr  33948  hgt750lem  34808  cusgracyclt3v  35350  sinccvglem  35866  mblfinlem3  37860  itg2addnclem2  37873  itg2addnclem3  37874  3rdpwhole  42547  tan3rdpi  42607  sin2t3rdpi  42608  cos2t3rdpi  42609  sin4t3rdpi  42610  cos4t3rdpi  42611  acos1half  42613  3cubeslem2  42927  lhe4.4ex1a  44570  stoweidlem11  46255  stoweidlem13  46257  stoweidlem26  46270  stoweidlem34  46278  stoweidlem42  46286  stoweidlem59  46303  stoweidlem62  46306  stoweid  46307  wallispilem4  46312  wallispi2lem1  46315  stirlinglem11  46328  fourierdlem87  46437  usgrexmpl2lem  48272  usgrexmpl2nb3  48280  usgrexmpl2trifr  48283  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem4  48365  itcoval3  48911  sepfsepc  49173