Metamath Proof Explorer


Theorem 4t5e20

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

Ref Expression
Assertion 4t5e20 4 5 = 20

Proof

Step Hyp Ref Expression
1 5cn 5
2 4cn 4
3 5t4e20 5 4 = 20
4 1 2 3 mulcomli 4 5 = 20