Description: The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | 4bc3eq4 | |- ( 4 _C 3 ) = 4 |
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 |