Theorem 2t2e4 12429

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 12403	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 12400	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2783	1 ⊢ (2 · 2) = 4

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7414   + caddc 11128   · cmul 11130  2c2 12320  4c4 12322

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-mulcl 11187  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-1rid 11195  ax-cnre 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-2 12328  df-3 12329  df-4 12330

This theorem is used by:  4div2e2  12437  div4p1lem1div2  12524  3halfnz  12701  decbin0  12884  fldiv4lem1div2uz2  13898  sq2  14262  sq4e2t8  14264  discr  14305  sqoddm1div8  14308  faclbnd2  14356  4bc2eq6  14394  amgm2  15458  bpoly3  16145  sin4lt0  16284  z4even  16463  flodddiv4  16506  flodddiv4t2lthalf  16509  4nprm  16786  2exp4  17177  2exp16  17183  5prm  17201  631prm  17220  1259lem1  17224  1259lem4  17227  2503lem1  17230  2503lem2  17231  2503lem3  17232  4001lem1  17234  4001lem2  17235  4001lem3  17236  4001prm  17238  pcoass  25253  minveclem2  25655  uniioombllem5  25816  uniioombl  25818  dveflem  26207  pilem2  26689  sinhalfpilem  26702  sincosq1lem  26736  tangtx  26744  sincos4thpi  26752  heron  27076  quad2  27077  dquartlem1  27089  dquart  27091  quart1  27094  atan1  27166  log2ublem3  27186  log2ub  27187  chtub  27449  bclbnd  27517  bpos1  27520  bposlem2  27522  bposlem6  27526  bposlem9  27529  gausslemma2dlem3  27605  m1lgs  27625  2lgslem1a2  27627  2lgslem3a  27633  2lgslem3b  27634  2lgslem3c  27635  2lgslem3d  27636  pntibndlem2  27828  pntlemg  27835  pntlemr  27839  ex-fl  30928  minvecolem2  31357  polid2i  31639  binom2subadd  33213  quad3d  33221  quad3  36250  420lcm8e840  42878  3exp7  42920  3lexlogpow5ineq1  42921  3lexlogpow2ineq2  42926  3lexlogpow5ineq5  42927  aks4d1p1p2  42937  aks4d1p1  42943  2ap1caineq  43012  25or6to4  43073  cxpi11d  43219  flt4lem  43492  3cubeslem3l  43532  3cubeslem3r  43533  wallispi2lem1  46900  wallispi2lem2  46901  stirlinglem3  46905  stirlinglem10  46912  sin5tlem2  47739  cos5t  47744  goldpolyfactor  47746  2ltceilhalf  48221  ceil5half3  48235  modmkpkne  48256  fmtnorec4  48453  nprmdvdsfacm1lem4  48527  ppivalnn4  48531  2exp340mod341  48650  8exp8mod9  48653  ackval2012  49622