Theorem 4t2e8 12129

Description: 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
4t2e8	⊢ (4 · 2) = 8

Proof of Theorem 4t2e8

Step	Hyp	Ref	Expression
1		4cn 12046	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12100	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12116	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2766	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1539  (class class class)co 7268   + caddc 10862   · cmul 10864  2c2 12016  4c4 12018  8c8 12022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10916  ax-1cn 10917  ax-icn 10918  ax-addcl 10919  ax-mulcl 10921  ax-mulcom 10923  ax-addass 10924  ax-mulass 10925  ax-distr 10926  ax-1rid 10929  ax-cnre 10932

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5075  df-iota 6385  df-fv 6435  df-ov 7271  df-2 12024  df-3 12025  df-4 12026  df-5 12027  df-6 12028  df-7 12029  df-8 12030

This theorem is referenced by:  8th4div3  12181  4t3e12  12523  sq4e2t8  13904  cu2  13905  sqoddm1div8  13946  cos2bnd  15885  2exp7  16777  2exp8  16778  8nprm  16801  19prm  16807  139prm  16813  1259lem2  16821  1259lem3  16822  1259lem4  16823  1259lem5  16824  2503lem1  16826  2503lem2  16827  4001lem1  16830  4001lem2  16831  4001lem3  16832  4001lem4  16833  quart1lem  25993  quart1  25994  quartlem1  25995  log2tlbnd  26083  log2ub  26087  bpos1  26419  bposlem8  26427  lgsdir2lem2  26462  2lgslem3a  26532  2lgslem3b  26533  2lgslem3c  26534  2lgslem3d  26535  2lgsoddprmlem2  26545  2lgsoddprmlem3c  26548  2lgsoddprmlem3d  26549  chebbnd1lem2  26606  chebbnd1lem3  26607  pntlemr  26738  ex-exp  28800  420gcd8e4  40000  420lcm8e840  40005  lcmineqlem23  40045  3lexlogpow2ineq2  40053  fmtno4prmfac  44980  139prmALT  45004  mod42tp1mod8  45010  3exp4mod41  45024  41prothprm  45027  8even  45121  2exp340mod341  45141  8exp8mod9  45144