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