Theorem 3elfz13

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

	Ref	Expression
Assertion	3elfz13	$$⊢3\in \left(1\dots 3\right)$$

Proof

Step	Hyp	Ref	Expression
1		3nn	$$⊢3\in \mathbb{N}$$
2		elfz1end	$$⊢3\in \mathbb{N}\leftrightarrow 3\in \left(1\dots 3\right)$$
3	1 2	mpbi	$$⊢3\in \left(1\dots 3\right)$$