Metamath Proof Explorer

Theorem 3elfz13

Description: Membership of 3 in the integer interval ( 1 ... 3 ). (Contributed by Jiamin Zhao, 1-Aug-2026)

Ref Expression
Assertion 3elfz13 
|- 3 e. ( 1 ... 3 )

Proof

Step Hyp Ref Expression
1 3nn 
 |-  3 e. NN
2 elfz1end 
 |-  ( 3 e. NN <-> 3 e. ( 1 ... 3 ) )
3 1 2 mpbi 
 |-  3 e. ( 1 ... 3 )