Theorem 2t2e4 12340

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 12256	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12314	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12311	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2759	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7367   + caddc 11041   · cmul 11043  2c2 12236  4c4 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246

This theorem is referenced by:  4div2e2  12346  div4p1lem1div2  12432  3halfnz  12608  decbin0  12784  fldiv4lem1div2uz2  13795  sq2  14159  sq4e2t8  14161  discr  14202  sqoddm1div8  14205  faclbnd2  14253  4bc2eq6  14291  amgm2  15332  bpoly3  16023  sin4lt0  16162  z4even  16341  flodddiv4  16384  flodddiv4t2lthalf  16387  4nprm  16664  2exp4  17055  2exp16  17061  5prm  17079  631prm  17097  1259lem1  17101  1259lem4  17104  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001prm  17115  pcoass  24991  minveclem2  25393  uniioombllem5  25554  uniioombl  25556  dveflem  25946  pilem2  26417  sinhalfpilem  26427  sincosq1lem  26461  tangtx  26469  sincos4thpi  26477  heron  26802  quad2  26803  dquartlem1  26815  dquart  26817  quart1  26820  atan1  26892  log2ublem3  26912  log2ub  26913  chtub  27175  bclbnd  27243  bpos1  27246  bposlem2  27248  bposlem6  27252  bposlem9  27255  gausslemma2dlem3  27331  m1lgs  27351  2lgslem1a2  27353  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  pntibndlem2  27554  pntlemg  27561  pntlemr  27565  ex-fl  30517  minvecolem2  30946  polid2i  31228  binom2subadd  32814  quad3d  32822  quad3  35852  420lcm8e840  42450  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1p1p2  42509  aks4d1p1  42515  2ap1caineq  42584  cxpi11d  42775  flt4lem  43078  3cubeslem3l  43118  3cubeslem3r  43119  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem3  46504  stirlinglem10  46511  sin5tlem2  47322  cos5t  47327  2ltceilhalf  47780  ceil5half3  47794  modmkpkne  47815  fmtnorec4  48012  nprmdvdsfacm1lem4  48086  ppivalnn4  48090  2exp340mod341  48209  8exp8mod9  48212  ackval2012  49167