![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 4t2e8 | Structured version Visualization version GIF version |
Description: 4 times 2 equals 8. (Contributed by NM, 2-Aug-2004.) |
Ref | Expression |
---|---|
4t2e8 | ⊢ (4 · 2) = 8 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4cn 12333 | . . 3 ⊢ 4 ∈ ℂ | |
2 | 1 | times2i 12387 | . 2 ⊢ (4 · 2) = (4 + 4) |
3 | 4p4e8 12403 | . 2 ⊢ (4 + 4) = 8 | |
4 | 2, 3 | eqtri 2755 | 1 ⊢ (4 · 2) = 8 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 (class class class)co 7424 + caddc 11147 · cmul 11149 2c2 12303 4c4 12305 8c8 12309 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-resscn 11201 ax-1cn 11202 ax-icn 11203 ax-addcl 11204 ax-mulcl 11206 ax-mulcom 11208 ax-addass 11209 ax-mulass 11210 ax-distr 11211 ax-1rid 11214 ax-cnre 11217 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-iota 6503 df-fv 6559 df-ov 7427 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 |
This theorem is referenced by: 8th4div3 12468 4t3e12 12811 sq4e2t8 14200 cu2 14201 sqoddm1div8 14243 cos2bnd 16170 2exp7 17062 2exp8 17063 8nprm 17086 19prm 17092 139prm 17098 1259lem2 17106 1259lem3 17107 1259lem4 17108 1259lem5 17109 2503lem1 17111 2503lem2 17112 4001lem1 17115 4001lem2 17116 4001lem3 17117 4001lem4 17118 quart1lem 26805 quart1 26806 quartlem1 26807 log2tlbnd 26895 log2ub 26899 bpos1 27234 bposlem8 27242 lgsdir2lem2 27277 2lgslem3a 27347 2lgslem3b 27348 2lgslem3c 27349 2lgslem3d 27350 2lgsoddprmlem2 27360 2lgsoddprmlem3c 27363 2lgsoddprmlem3d 27364 chebbnd1lem2 27421 chebbnd1lem3 27422 pntlemr 27553 ex-exp 30278 420gcd8e4 41481 420lcm8e840 41486 lcmineqlem23 41526 3lexlogpow2ineq2 41534 sum9cubes 42099 fmtno4prmfac 46914 139prmALT 46938 mod42tp1mod8 46944 3exp4mod41 46958 41prothprm 46961 8even 47055 2exp340mod341 47075 8exp8mod9 47078 |
Copyright terms: Public domain | W3C validator |