Theorem 4even

Description: 4 is an even number. (Contributed by AV, 23-Jul-2020)

	Ref	Expression
Assertion	4even	$$⊢4\in \mathrm{Even}$$

Proof

Step	Hyp	Ref	Expression
1		3odd	$$⊢3\in \mathrm{Odd}$$
2		df-4	$$⊢4=3+1$$
3		oddp1eveni	$$⊢3\in \mathrm{Odd}\to 3+1\in \mathrm{Even}$$
4	2 3	eqeltrid	$$⊢3\in \mathrm{Odd}\to 4\in \mathrm{Even}$$
5	1 4	ax-mp	$$⊢4\in \mathrm{Even}$$