This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4even

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

		Ref	Expression
	Assertion	4even	$⊢ 4 \in Even$

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