Theorem 4bc3eq4

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

	Ref	Expression
Assertion	4bc3eq4	⊢ ( 4 C 3 ) = 4

Proof

Step	Hyp	Ref	Expression
1		4m1e3	⊢ ( 4 − 1 ) = 3
2	1	oveq2i	⊢ ( 4 C ( 4 − 1 ) ) = ( 4 C 3 )
3		4nn0	⊢ 4 ∈ ℕ0
4		bcnm1	⊢ ( 4 ∈ ℕ0 → ( 4 C ( 4 − 1 ) ) = 4 )
5	3 4	ax-mp	⊢ ( 4 C ( 4 − 1 ) ) = 4
6	2 5	eqtr3i	⊢ ( 4 C 3 ) = 4