Theorem 7odd

Description: 7 is an odd number. (Contributed by AV, 20-Jul-2020)

	Ref	Expression
Assertion	7odd	$$⊢7\in \mathrm{Odd}$$

Proof

Step	Hyp	Ref	Expression
1		df-7	$$⊢7=6+1$$
2		6even	$$⊢6\in \mathrm{Even}$$
3		evenp1odd	$$⊢6\in \mathrm{Even}\to 6+1\in \mathrm{Odd}$$
4	2 3	ax-mp	$$⊢6+1\in \mathrm{Odd}$$
5	1 4	eqeltri	$$⊢7\in \mathrm{Odd}$$