![]() |
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 11293 | . . 3 ⊢ 2 ∈ ℂ | |
2 | 1 | 2timesi 11349 | . 2 ⊢ (2 · 2) = (2 + 2) |
3 | 2p2e4 11346 | . 2 ⊢ (2 + 2) = 4 | |
4 | 2, 3 | eqtri 2793 | 1 ⊢ (2 · 2) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 (class class class)co 6793 + caddc 10141 · cmul 10143 2c2 11272 4c4 11274 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-resscn 10195 ax-1cn 10196 ax-icn 10197 ax-addcl 10198 ax-addrcl 10199 ax-mulcl 10200 ax-mulrcl 10201 ax-mulcom 10202 ax-addass 10203 ax-mulass 10204 ax-distr 10205 ax-i2m1 10206 ax-1ne0 10207 ax-1rid 10208 ax-rrecex 10210 ax-cnre 10211 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-iota 5994 df-fv 6039 df-ov 6796 df-2 11281 df-3 11282 df-4 11283 |
This theorem is referenced by: 4d2e2 11386 halfpm6th 11455 div4p1lem1div2 11489 3halfnz 11658 decbin0 11883 fldiv4lem1div2uz2 12845 sq2 13167 sq4e2t8 13169 discr 13208 sqoddm1div8 13235 faclbnd2 13282 4bc2eq6 13320 amgm2 14317 bpoly3 14995 sin4lt0 15131 z4even 15316 flodddiv4 15345 flodddiv4t2lthalf 15348 4nprm 15614 2exp4 16001 2exp16 16004 5prm 16022 631prm 16041 1259lem1 16045 1259lem4 16048 2503lem1 16051 2503lem2 16052 2503lem3 16053 4001lem1 16055 4001lem2 16056 4001lem3 16057 4001prm 16059 pcoass 23043 minveclem2 23416 uniioombllem5 23575 uniioombl 23577 dveflem 23962 pilem2 24426 sinhalfpilem 24436 sincosq1lem 24470 tangtx 24478 sincos4thpi 24486 heron 24786 quad2 24787 dquartlem1 24799 dquart 24801 quart1 24804 atan1 24876 log2ublem3 24896 log2ub 24897 ppiublem2 25149 chtub 25158 bclbnd 25226 bpos1 25229 bposlem2 25231 bposlem6 25235 bposlem9 25238 gausslemma2dlem3 25314 m1lgs 25334 2lgslem1a2 25336 2lgslem3a 25342 2lgslem3b 25343 2lgslem3c 25344 2lgslem3d 25345 pntibndlem2 25501 pntlemg 25508 pntlemr 25512 ex-fl 27646 minvecolem2 28071 polid2i 28354 quad3 31902 wallispi2lem1 40805 wallispi2lem2 40806 stirlinglem3 40810 stirlinglem10 40817 fmtnorec4 41989 |
Copyright terms: Public domain | W3C validator |