Theorem 2t2e4 9409

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

Assertion

Ref	Expression
2t2e4	⊢ (2 · 2) = 4

Proof of Theorem 2t2e4

Step	Hyp	Ref	Expression
1		2cn 9325	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 9384	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 9381	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2255	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1398  (class class class)co 6058   + caddc 8146   · cmul 8148  2c2 9305  4c4 9307

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235  ax-1cn 8236  ax-1re 8237  ax-icn 8238  ax-addcl 8239  ax-addrcl 8240  ax-mulcl 8241  ax-mulcom 8244  ax-addass 8245  ax-mulass 8246  ax-distr 8247  ax-1rid 8250  ax-cnre 8254

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-2 9313  df-3 9314  df-4 9315

This theorem is referenced by:  4d2e2  9415  halfpm6th  9475  div4p1lem1div2  9509  3halfnz  9693  decbin0  9866  fldiv4lem1div2uz2  10690  sq2  11021  sq4e2t8  11023  sqoddm1div8  11080  faclbnd2  11129  4bc2eq6  11162  amgm2  11828  sin4lt0  12478  z4even  12627  flodddiv4  12647  flodddiv4t2lthalf  12650  4nprm  12851  2exp4  13154  2exp16  13160  dveflem  15717  sin0pilem2  15773  sinhalfpilem  15782  sincosq1lem  15816  tangtx  15829  sincos4thpi  15831  gausslemma2dlem3  16062  m1lgs  16084  2lgslem1a2  16086  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  ex-fl  16619