Theorem 2t2e4 12345

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 12261	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12319	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12316	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2752	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7387   + caddc 11071   · cmul 11073  2c2 12241  4c4 12243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251

This theorem is referenced by:  4d2e2  12351  div4p1lem1div2  12437  3halfnz  12613  decbin0  12789  fldiv4lem1div2uz2  13798  sq2  14162  sq4e2t8  14164  discr  14205  sqoddm1div8  14208  faclbnd2  14256  4bc2eq6  14294  amgm2  15336  bpoly3  16024  sin4lt0  16163  z4even  16342  flodddiv4  16385  flodddiv4t2lthalf  16388  4nprm  16665  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  24924  minveclem2  25326  uniioombllem5  25488  uniioombl  25490  dveflem  25883  pilem2  26362  sinhalfpilem  26372  sincosq1lem  26406  tangtx  26414  sincos4thpi  26422  heron  26748  quad2  26749  dquartlem1  26761  dquart  26763  quart1  26766  atan1  26838  log2ublem3  26858  log2ub  26859  chtub  27123  bclbnd  27191  bpos1  27194  bposlem2  27196  bposlem6  27200  bposlem9  27203  gausslemma2dlem3  27279  m1lgs  27299  2lgslem1a2  27301  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  pntibndlem2  27502  pntlemg  27509  pntlemr  27513  ex-fl  30376  minvecolem2  30804  polid2i  31086  binom2subadd  32665  quad3d  32673  quad3  35657  420lcm8e840  41999  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p2  42058  aks4d1p1  42064  2ap1caineq  42133  cxpi11d  42331  flt4lem  42633  3cubeslem3l  42674  3cubeslem3r  42675  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem3  46074  stirlinglem10  46081  2ltceilhalf  47329  ceil5half3  47341  modmkpkne  47362  fmtnorec4  47550  2exp340mod341  47734  8exp8mod9  47737  ackval2012  48680