Theorem 2t2e4 9071

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 8988	. . 3 ⊢ 2 ∈ ℂ
2	1	2timesi 9047	. 2 ⊢ (2 · 2) = (2 + 2)
3		2p2e4 9044	. 2 ⊢ (2 + 2) = 4
4	2, 3	eqtri 2198	1 ⊢ (2 · 2) = 4

Syntax hints:   = wceq 1353  (class class class)co 5874   + caddc 7813   · cmul 7815  2c2 8968  4c4 8970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-1rid 7917  ax-cnre 7921

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-2 8976  df-3 8977  df-4 8978

This theorem is referenced by:  4d2e2  9077  halfpm6th  9137  div4p1lem1div2  9170  3halfnz  9348  decbin0  9521  sq2  10612  sq4e2t8  10614  sqoddm1div8  10670  faclbnd2  10717  4bc2eq6  10749  amgm2  11122  sin4lt0  11769  z4even  11915  flodddiv4  11933  flodddiv4t2lthalf  11936  4nprm  12123  dveflem  14080  sin0pilem2  14096  sinhalfpilem  14105  sincosq1lem  14139  tangtx  14152  sincos4thpi  14154  ex-fl  14359