Theorem 4t2e8 12404

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 12321	. . 3 ⊢ 4 ∈ ℂ
2	1	times2i 12374	. 2 ⊢ (4 · 2) = (4 + 4)
3		4p4e8 12390	. 2 ⊢ (4 + 4) = 8
4	2, 3	eqtri 2786	1 ⊢ (4 · 2) = 8

Syntax hints:   = wceq 1570  (class class class)co 7410   + caddc 11098   · cmul 11100  2c2 12290  4c4 12292  8c8 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-1rid 11165  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304

This theorem is referenced by:  2t4e8  12405  8th4div3  12459  4t3e12  12809  sq4e2t8  14231  cu2  14232  sqoddm1div8  14275  cos2bnd  16239  2exp7  17142  2exp8  17143  8nprm  17166  19prm  17173  139prm  17179  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem1  17192  2503lem2  17193  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  quart1lem  27020  quart1  27021  quartlem1  27022  log2tlbnd  27110  log2ub  27114  bpos1  27447  bposlem8  27455  lgsdir2lem2  27490  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2lgsoddprmlem2  27573  2lgsoddprmlem3c  27576  2lgsoddprmlem3d  27577  chebbnd1lem2  27634  chebbnd1lem3  27635  pntlemr  27766  ex-exp  30801  420gcd8e4  42773  420lcm8e840  42778  lcmineqlem23  42818  3lexlogpow2ineq2  42826  sum9cubes  43404  sin5tlem4  47613  goldratmolem2  47623  fmtno4prmfac  48324  139prmALT  48348  3exp4mod41  48368  41prothprm  48371  8even  48478  2exp340mod341  48498  8exp8mod9  48501  pgnbgreunbgrlem4  48884