Metamath Proof Explorer

Theorem znod

Description: A surreal integer is a surreal. Deduction form. (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Hypothesis znod.1 
|- ( ph -> A e. ZZ_s )
Assertion znod 
|- ( ph -> A e. No )

Proof

Step Hyp Ref Expression
1 znod.1 
 |-  ( ph -> A e. ZZ_s )
2 zno 
 |-  ( A e. ZZ_s -> A e. No )
3 1 2 syl 
 |-  ( ph -> A e. No )