![]() |
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 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 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |