Theorem 4even

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

	Ref	Expression
Assertion	4even	⊢ 4 ∈ Even

Proof

Step	Hyp	Ref	Expression
1		3odd	⊢ 3 ∈ Odd
2		df-4	⊢ 4 = ( 3 + 1 )
3		oddp1eveni	⊢ ( 3 ∈ Odd → ( 3 + 1 ) ∈ Even )
4	2 3	eqeltrid	⊢ ( 3 ∈ Odd → 4 ∈ Even )
5	1 4	ax-mp	⊢ 4 ∈ Even