Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2t2e4 | 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 8919 | . . 3 ⊢ 2 ∈ ℂ | |
2 | 1 | 2timesi 8978 | . 2 ⊢ (2 · 2) = (2 + 2) |
3 | 2p2e4 8975 | . 2 ⊢ (2 + 2) = 4 | |
4 | 2, 3 | eqtri 2185 | 1 ⊢ (2 · 2) = 4 |
Colors of variables: wff set class |
Syntax hints: = wceq 1342 (class class class)co 5836 + caddc 7747 · cmul 7749 2c2 8899 4c4 8901 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-resscn 7836 ax-1cn 7837 ax-1re 7838 ax-icn 7839 ax-addcl 7840 ax-addrcl 7841 ax-mulcl 7842 ax-mulcom 7845 ax-addass 7846 ax-mulass 7847 ax-distr 7848 ax-1rid 7851 ax-cnre 7855 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-rex 2448 df-v 2723 df-un 3115 df-in 3117 df-ss 3124 df-sn 3576 df-pr 3577 df-op 3579 df-uni 3784 df-br 3977 df-iota 5147 df-fv 5190 df-ov 5839 df-2 8907 df-3 8908 df-4 8909 |
This theorem is referenced by: 4d2e2 9008 halfpm6th 9068 div4p1lem1div2 9101 3halfnz 9279 decbin0 9452 sq2 10540 sq4e2t8 10542 sqoddm1div8 10597 faclbnd2 10644 4bc2eq6 10676 amgm2 11046 sin4lt0 11693 z4even 11838 flodddiv4 11856 flodddiv4t2lthalf 11859 4nprm 12040 dveflem 13228 sin0pilem2 13244 sinhalfpilem 13253 sincosq1lem 13287 tangtx 13300 sincos4thpi 13302 ex-fl 13443 |
Copyright terms: Public domain | W3C validator |