![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2t2e4 | Structured version Visualization version GIF version |
Description: 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
Ref | Expression |
---|---|
2t2e4 | ⊢ (2 · 2) = 4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 11388 | . . 3 ⊢ 2 ∈ ℂ | |
2 | 1 | 2timesi 11458 | . 2 ⊢ (2 · 2) = (2 + 2) |
3 | 2p2e4 11455 | . 2 ⊢ (2 + 2) = 4 | |
4 | 2, 3 | eqtri 2821 | 1 ⊢ (2 · 2) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 (class class class)co 6878 + caddc 10227 · cmul 10229 2c2 11368 4c4 11370 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-mulcl 10286 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-1rid 10294 ax-cnre 10297 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-iota 6064 df-fv 6109 df-ov 6881 df-2 11376 df-3 11377 df-4 11378 |
This theorem is referenced by: 4d2e2 11490 halfpm6th 11541 div4p1lem1div2 11575 3halfnz 11746 decbin0 11925 fldiv4lem1div2uz2 12892 sq2 13214 sq4e2t8 13216 discr 13255 sqoddm1div8 13284 faclbnd2 13331 4bc2eq6 13369 amgm2 14450 bpoly3 15125 sin4lt0 15261 z4even 15444 flodddiv4 15472 flodddiv4t2lthalf 15475 4nprm 15741 2exp4 16122 2exp16 16125 5prm 16143 631prm 16161 1259lem1 16165 1259lem4 16168 2503lem1 16171 2503lem2 16172 2503lem3 16173 4001lem1 16175 4001lem2 16176 4001lem3 16177 4001prm 16179 pcoass 23151 minveclem2 23536 uniioombllem5 23695 uniioombl 23697 dveflem 24083 pilem2 24547 sinhalfpilem 24557 sincosq1lem 24591 tangtx 24599 sincos4thpi 24607 heron 24917 quad2 24918 dquartlem1 24930 dquart 24932 quart1 24935 atan1 25007 log2ublem3 25027 log2ub 25028 ppiublem2 25280 chtub 25289 bclbnd 25357 bpos1 25360 bposlem2 25362 bposlem6 25366 bposlem9 25369 gausslemma2dlem3 25445 m1lgs 25465 2lgslem1a2 25467 2lgslem3a 25473 2lgslem3b 25474 2lgslem3c 25475 2lgslem3d 25476 pntibndlem2 25632 pntlemg 25639 pntlemr 25643 ex-fl 27832 minvecolem2 28256 polid2i 28539 quad3 32079 wallispi2lem1 41031 wallispi2lem2 41032 stirlinglem3 41036 stirlinglem10 41043 fmtnorec4 42243 |
Copyright terms: Public domain | W3C validator |