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

Metamath Proof Explorer

Theorem 4bc3eq4

Description: The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016)

		Ref	Expression
	Assertion	4bc3eq4	$⊢ (\binom{4}{3}) = 4$

Step	Hyp	Ref	Expression
1		4m1e3	$⊢ 4 - 1 = 3$
2	1	oveq2i	$⊢ (\binom{4}{4 - 1}) = (\binom{4}{3})$
3		4nn0	$⊢ 4 \in ℕ_{0}$
4		bcnm1	$⊢ 4 \in ℕ_{0} \to (\binom{4}{4 - 1}) = 4$
5	3 4	ax-mp	$⊢ (\binom{4}{4 - 1}) = 4$
6	2 5	eqtr3i	$⊢ (\binom{4}{3}) = 4$