Theorem 2t2e4 9072

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

Assertion

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

Proof of Theorem 2t2e4

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

Syntax hints:   = wceq 1353  (class class class)co 5874   + caddc 7813   x. cmul 7815   2c2 8969   4c4 8971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-1rid 7917  ax-cnre 7921

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-2 8977  df-3 8978  df-4 8979

This theorem is referenced by:  4d2e2  9078  halfpm6th  9138  div4p1lem1div2  9171  3halfnz  9349  decbin0  9522  sq2  10615  sq4e2t8  10617  sqoddm1div8  10673  faclbnd2  10721  4bc2eq6  10753  amgm2  11126  sin4lt0  11773  z4even  11920  flodddiv4  11938  flodddiv4t2lthalf  11941  4nprm  12128  dveflem  14157  sin0pilem2  14173  sinhalfpilem  14182  sincosq1lem  14216  tangtx  14229  sincos4thpi  14231  m1lgs  14422  ex-fl  14447