Theorem 4t5e20

Description: 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025)

	Ref	Expression
Assertion	4t5e20	|- ( 4 x. 5 ) = ; 2 0

Proof

Step	Hyp	Ref	Expression
1		5cn	|- 5 e. CC
2		4cn	|- 4 e. CC
3		5t4e20	|- ( 5 x. 4 ) = ; 2 0
4	1 2 3	mulcomli	|- ( 4 x. 5 ) = ; 2 0