![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2timesd | GIF version |
Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
2timesd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
2timesd | ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2timesd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | 2times 8605 | . 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1290 ∈ wcel 1439 (class class class)co 5666 ℂcc 7409 + caddc 7414 · cmul 7416 2c2 8534 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-resscn 7498 ax-1cn 7499 ax-icn 7501 ax-addcl 7502 ax-mulcl 7504 ax-mulcom 7507 ax-mulass 7509 ax-distr 7510 ax-1rid 7513 ax-cnre 7517 |
This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-rex 2366 df-v 2622 df-un 3004 df-in 3006 df-ss 3013 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-br 3852 df-iota 4993 df-fv 5036 df-ov 5669 df-2 8542 |
This theorem is referenced by: fzctr 9605 flhalf 9770 q2submod 9853 modaddmodup 9855 m1expeven 10063 binom2 10126 nn0opthlem2d 10190 crre 10352 imval2 10389 resqrexlemdec 10505 amgm2 10612 maxabsle 10698 maxabslemab 10700 maxltsup 10712 max0addsup 10713 arisum2 10954 efival 11084 sinadd 11088 cosadd 11089 addsin 11094 subsin 11095 cosmul 11097 addcos 11098 subcos 11099 sin2t 11101 cos2t 11102 eirraplem 11125 |
Copyright terms: Public domain | W3C validator |