Theorem 2t2e4 11789

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 11700	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 11763	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 11760	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2821	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1538  (class class class)co 7135   + caddc 10529   · cmul 10531  2c2 11680  4c4 11682

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688  df-3 11689  df-4 11690

This theorem is referenced by:  4d2e2  11795  halfpm6th  11846  div4p1lem1div2  11880  3halfnz  12049  decbin0  12226  fldiv4lem1div2uz2  13201  sq2  13556  sq4e2t8  13558  discr  13597  sqoddm1div8  13600  faclbnd2  13647  4bc2eq6  13685  amgm2  14721  bpoly3  15404  sin4lt0  15540  z4even  15713  flodddiv4  15754  flodddiv4t2lthalf  15757  4nprm  16029  2exp4  16411  2exp16  16416  5prm  16434  631prm  16452  1259lem1  16456  1259lem4  16459  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001prm  16470  pcoass  23629  minveclem2  24030  uniioombllem5  24191  uniioombl  24193  dveflem  24582  pilem2  25047  sinhalfpilem  25056  sincosq1lem  25090  tangtx  25098  sincos4thpi  25106  heron  25424  quad2  25425  dquartlem1  25437  dquart  25439  quart1  25442  atan1  25514  log2ublem3  25534  log2ub  25535  chtub  25796  bclbnd  25864  bpos1  25867  bposlem2  25869  bposlem6  25873  bposlem9  25876  gausslemma2dlem3  25952  m1lgs  25972  2lgslem1a2  25974  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  pntibndlem2  26175  pntlemg  26182  pntlemr  26186  ex-fl  28232  minvecolem2  28658  polid2i  28940  quad3  33026  420lcm8e840  39299  3lexlogpow5ineq1  39341  2ap1caineq  39349  3cubeslem3l  39627  3cubeslem3r  39628  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem3  42718  stirlinglem10  42725  fmtnorec4  44066  2exp340mod341  44251  8exp8mod9  44254  ackval2012  45105