Metamath Proof Explorer

Theorem 2t2e4

Description: 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999)

Ref Expression
Assertion 2t2e4 
|- ( 2 x. 2 ) = 4

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 1 2timesi 
 |-  ( 2 x. 2 ) = ( 2 + 2 )
3 2p2e4 
 |-  ( 2 + 2 ) = 4
4 2 3 eqtri 
 |-  ( 2 x. 2 ) = 4