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!=\left(2+1\right)!$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4		facp1	$$⊢2\in {\mathbb{N}}_0\to \left(2+1\right)!=2!\left(2+1\right)$$
5	3 4	ax-mp	$$⊢\left(2+1\right)!=2!\left(2+1\right)$$
6		fac2	$$⊢2!=2$$
7		2p1e3	$$⊢2+1=3$$
8	6 7	oveq12i	$$⊢2!\left(2+1\right)=2\cdot 3$$
9		2t3e6	$$⊢2\cdot 3=6$$
10	8 9	eqtri	$$⊢2!\left(2+1\right)=6$$
11	2 5 10	3eqtri	$$⊢3!=6$$