Metamath Proof Explorer


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 e. NN0
4 bcnm1
 |-  ( 4 e. NN0 -> ( 4 _C ( 4 - 1 ) ) = 4 )
5 3 4 ax-mp
 |-  ( 4 _C ( 4 - 1 ) ) = 4
6 2 5 eqtr3i
 |-  ( 4 _C 3 ) = 4