Theorem 4t2e8 11526

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 11437	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 11497	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 11513	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2849	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1658  (class class class)co 6905   + caddc 10255   · cmul 10257  2c2 11406  4c4 11408  8c8 11412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-mulcl 10314  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-1rid 10322  ax-cnre 10325

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420

This theorem is referenced by:  8th4div3  11578  4t3e12  11921  sq4e2t8  13256  cu2  13257  sqoddm1div8  13324  cos2bnd  15290  2exp8  16162  8nprm  16184  19prm  16190  139prm  16196  1259lem2  16204  1259lem3  16205  1259lem4  16206  1259lem5  16207  2503lem1  16209  2503lem2  16210  4001lem1  16213  4001lem2  16214  4001lem3  16215  4001lem4  16216  quart1lem  24995  quart1  24996  quartlem1  24997  log2tlbnd  25085  log2ub  25089  bpos1  25421  bposlem8  25429  lgsdir2lem2  25464  2lgslem3a  25534  2lgslem3b  25535  2lgslem3c  25536  2lgslem3d  25537  2lgsoddprmlem2  25547  2lgsoddprmlem3c  25550  2lgsoddprmlem3d  25551  chebbnd1lem2  25572  chebbnd1lem3  25573  pntlemr  25704  ex-exp  27865  fmtno4prmfac  42314  139prmALT  42341  2exp7  42344  mod42tp1mod8  42349  3exp4mod41  42363  41prothprm  42366  8even  42452