Metamath Proof Explorer


Theorem nosgnn0i

Description: If X is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011)

Ref Expression
Hypothesis nosgnn0i.1 X 1 𝑜 2 𝑜
Assertion nosgnn0i X

Proof

Step Hyp Ref Expression
1 nosgnn0i.1 X 1 𝑜 2 𝑜
2 nosgnn0 ¬ 1 𝑜 2 𝑜
3 eleq1 = X 1 𝑜 2 𝑜 X 1 𝑜 2 𝑜
4 1 3 mpbiri = X 1 𝑜 2 𝑜
5 2 4 mto ¬ = X
6 5 neir X