Metamath Proof Explorer


Theorem 4bc3eq4

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

Ref Expression
Assertion 4bc3eq4 ( 4 3 ) = 4

Proof

Step Hyp Ref Expression
1 4m1e3 4 1 = 3
2 1 oveq2i ( 4 4 1 ) = ( 4 3 )
3 4nn0 4 0
4 bcnm1 4 0 ( 4 4 1 ) = 4
5 3 4 ax-mp ( 4 4 1 ) = 4
6 2 5 eqtr3i ( 4 3 ) = 4