Theorem 3elfz13

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

	Ref	Expression
Assertion	3elfz13	⊢ 3 ∈ ( 1 ... 3 )

Proof

Step	Hyp	Ref	Expression
1		3nn	⊢ 3 ∈ ℕ
2		elfz1end	⊢ ( 3 ∈ ℕ ↔ 3 ∈ ( 1 ... 3 ) )
3	1 2	mpbi	⊢ 3 ∈ ( 1 ... 3 )