Theorem 3ne0 12185

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		3re 12159	. 2 ⊢ 3 ∈ ℝ
2		3pos 12184	. 2 ⊢ 0 < 3
3	1, 2	gt0ne0ii 11617	1 ⊢ 3 ≠ 0

Syntax hints:   ≠ wne 2941  0cc0 10977  3c3 12135

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-po 5537  df-so 5538  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-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-er 8574  df-en 8810  df-dom 8811  df-sdom 8812  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-2 12142  df-3 12143

This theorem is referenced by:  8th4div3  12299  halfpm6th  12300  halfthird  12686  f1oun2prg  14730  sqrlem7  15060  caurcvgr  15485  bpoly2  15867  bpoly3  15868  bpoly4  15869  sin01bnd  15994  cos01bnd  15995  cos1bnd  15996  cos2bnd  15997  sin01gt0  15999  cos01gt0  16000  rpnnen2lem3  16025  rpnnen2lem11  16033  tangtx  25768  sincos6thpi  25778  sincos3rdpi  25779  pigt3  25780  pige3ALT  25782  2logb9irrALT  26054  1cubr  26098  dcubic1lem  26099  dcubic2  26100  dcubic1  26101  dcubic  26102  mcubic  26103  cubic2  26104  cubic  26105  quartlem3  26115  log2cnv  26200  log2tlbnd  26201  ppiub  26458  bclbnd  26534  bposlem6  26543  bposlem9  26546  usgrexmplef  27915  upgr4cycl4dv4e  28837  konigsbergiedgw  28900  konigsberglem1  28904  konigsberglem3  28906  konigsberglem5  28908  ex-lcm  29110  hgt750lem  32929  cusgracyclt3v  33415  sinccvglem  33927  mblfinlem3  35970  itg2addnclem2  35983  itg2addnclem3  35984  acos1half  40476  3cubeslem2  40818  lhe4.4ex1a  42318  stoweidlem11  43938  stoweidlem13  43940  stoweidlem26  43953  stoweidlem34  43961  stoweidlem42  43969  stoweidlem59  43986  stoweidlem62  43989  stoweid  43990  wallispilem4  43995  wallispi2lem1  43998  stirlinglem11  44011  fourierdlem87  44120  itcoval3  46427  sepfsepc  46637