Theorem 2t2e4 12430

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 12341	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 12404	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12401	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2765	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7431   + caddc 11158   · cmul 11160  2c2 12321  4c4 12323

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331

This theorem is referenced by:  4d2e2  12436  halfpm6th  12487  div4p1lem1div2  12521  3halfnz  12697  decbin0  12873  fldiv4lem1div2uz2  13876  sq2  14236  sq4e2t8  14238  discr  14279  sqoddm1div8  14282  faclbnd2  14330  4bc2eq6  14368  amgm2  15408  bpoly3  16094  sin4lt0  16231  z4even  16409  flodddiv4  16452  flodddiv4t2lthalf  16455  4nprm  16732  2exp4  17122  2exp16  17128  5prm  17146  631prm  17164  1259lem1  17168  1259lem4  17171  2503lem1  17174  2503lem2  17175  2503lem3  17176  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001prm  17182  pcoass  25057  minveclem2  25460  uniioombllem5  25622  uniioombl  25624  dveflem  26017  pilem2  26496  sinhalfpilem  26505  sincosq1lem  26539  tangtx  26547  sincos4thpi  26555  heron  26881  quad2  26882  dquartlem1  26894  dquart  26896  quart1  26899  atan1  26971  log2ublem3  26991  log2ub  26992  chtub  27256  bclbnd  27324  bpos1  27327  bposlem2  27329  bposlem6  27333  bposlem9  27336  gausslemma2dlem3  27412  m1lgs  27432  2lgslem1a2  27434  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  pntibndlem2  27635  pntlemg  27642  pntlemr  27646  ex-fl  30466  minvecolem2  30894  polid2i  31176  quad3d  32754  quad3  35675  420lcm8e840  42012  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1p2  42071  aks4d1p1  42077  2ap1caineq  42146  cxpi11d  42379  flt4lem  42655  3cubeslem3l  42697  3cubeslem3r  42698  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem3  46091  stirlinglem10  46098  ceil5half3  47342  fmtnorec4  47536  2exp340mod341  47720  8exp8mod9  47723  2ltceilhalf  48015  ackval2012  48612