Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2t1e2 | Structured version Visualization version GIF version |
Description: 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Ref | Expression |
---|---|
2t1e2 | ⊢ (2 · 1) = 2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 10968 | . 2 ⊢ 2 ∈ ℂ | |
2 | 1 | mulid1i 9921 | 1 ⊢ (2 · 1) = 2 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 (class class class)co 6549 1c1 9816 · cmul 9820 2c2 10947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rrecex 9887 ax-cnre 9888 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 df-2 10956 |
This theorem is referenced by: decbin2 11559 expubnd 12783 sqrlem7 13837 trirecip 14434 bpoly3 14628 fsumcube 14630 ege2le3 14659 cos2tsin 14748 cos2bnd 14757 odd2np1 14903 opoe 14925 flodddiv4 14975 pythagtriplem4 15362 2503lem2 15683 2503lem3 15684 4001lem4 15689 4001prm 15690 htpycc 22587 pco1 22623 pcohtpylem 22627 pcopt 22630 pcorevlem 22634 ovolunlem1a 23071 cos2pi 24032 coskpi 24076 dcubic1lem 24370 dcubic2 24371 dcubic 24373 mcubic 24374 basellem3 24609 chtublem 24736 bcp1ctr 24804 bclbnd 24805 bposlem1 24809 bposlem2 24810 bposlem5 24813 2lgslem3d1 24928 chebbnd1lem1 24958 chebbnd1lem3 24960 chebbnd1 24961 frgraregord013 26645 ex-ind-dvds 26710 knoppndvlem12 31684 heiborlem6 32785 jm2.23 36581 sumnnodd 38697 wallispilem4 38961 wallispi2lem1 38964 wallispi2lem2 38965 wallispi2 38966 stirlinglem11 38977 dirkertrigeqlem1 38991 fouriersw 39124 fmtnorec4 39999 lighneallem2 40061 lighneallem3 40062 3exp4mod41 40071 opoeALTV 40132 av-frgraregord013 41549 |
Copyright terms: Public domain | W3C validator |