Theorem fac3

Description: The factorial of 3. (Contributed by NM, 17-Mar-2005)

	Ref	Expression
Assertion	fac3	|- ( ! ` 3 ) = 6

Proof

Step	Hyp	Ref	Expression
1		df-3	|- 3 = ( 2 + 1 )
2	1	fveq2i	|- ( ! ` 3 ) = ( ! ` ( 2 + 1 ) )
3		2nn0	|- 2 e. NN0
4		facp1	|- ( 2 e. NN0 -> ( ! ` ( 2 + 1 ) ) = ( ( ! ` 2 ) x. ( 2 + 1 ) ) )
5	3 4	ax-mp	|- ( ! ` ( 2 + 1 ) ) = ( ( ! ` 2 ) x. ( 2 + 1 ) )
6		fac2	|- ( ! ` 2 ) = 2
7		2p1e3	|- ( 2 + 1 ) = 3
8	6 7	oveq12i	|- ( ( ! ` 2 ) x. ( 2 + 1 ) ) = ( 2 x. 3 )
9		2t3e6	|- ( 2 x. 3 ) = 6
10	8 9	eqtri	|- ( ( ! ` 2 ) x. ( 2 + 1 ) ) = 6
11	2 5 10	3eqtri	|- ( ! ` 3 ) = 6