Theorem 7odd

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

	Ref	Expression
Assertion	7odd	⊢ 7 ∈ Odd

Proof

Step	Hyp	Ref	Expression
1		df-7	⊢ 7 = ( 6 + 1 )
2		6even	⊢ 6 ∈ Even
3		evenp1odd	⊢ ( 6 ∈ Even → ( 6 + 1 ) ∈ Odd )
4	2 3	ax-mp	⊢ ( 6 + 1 ) ∈ Odd
5	1 4	eqeltri	⊢ 7 ∈ Odd