This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3ne0

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

Ref Expression
Assertion 3ne0 
|- 3 =/= 0

Proof

Step Hyp Ref Expression
1 3nn 
 |-  3 e. NN
2 1 nnne0i 
 |-  3 =/= 0