![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulid2d | GIF version |
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
mulid2d | ⊢ (𝜑 → (1 · 𝐴) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | mullid 7957 | . 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ∈ wcel 2148 (class class class)co 5877 ℂcc 7811 1c1 7814 · cmul 7818 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-resscn 7905 ax-1cn 7906 ax-icn 7908 ax-addcl 7909 ax-mulcl 7911 ax-mulcom 7914 ax-mulass 7916 ax-distr 7917 ax-1rid 7920 ax-cnre 7924 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-v 2741 df-un 3135 df-in 3137 df-ss 3144 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-br 4006 df-iota 5180 df-fv 5226 df-ov 5880 |
This theorem is referenced by: adddirp1d 7986 mulsubfacd 8377 mulcanapd 8620 receuap 8628 divdivdivap 8672 divcanap5 8673 subrecap 8798 ltrec 8842 recp1lt1 8858 nndivtr 8963 xp1d2m1eqxm1d2 9173 gtndiv 9350 lincmb01cmp 10005 iccf1o 10006 modqfrac 10339 qnegmod 10371 addmodid 10374 m1expcl2 10544 expgt1 10560 ltexp2a 10574 leexp2a 10575 binom3 10640 faclbnd 10723 facavg 10728 bcval5 10745 cvg1nlemcau 10995 resqrexlemover 11021 resqrexlemcalc2 11026 absimle 11095 maxabslemlub 11218 reccn2ap 11323 binom1p 11495 binom1dif 11497 fprodsplitdc 11606 fprodcl2lem 11615 efcllemp 11668 ef01bndlem 11766 efieq1re 11781 eirraplem 11786 iddvds 11813 gcdaddm 11987 rpmulgcd 12029 prmind2 12122 isprm5lem 12143 phiprm 12225 eulerthlemth 12234 fermltl 12236 hashgcdlem 12240 odzdvds 12247 powm2modprm 12254 modprm0 12256 pythagtriplem4 12270 mulgnnass 13023 dvexp 14260 dvef 14273 reeff1oleme 14278 sin0pilem1 14287 sinhalfpip 14326 sinhalfpim 14327 coshalfpip 14328 coshalfpim 14329 tangtx 14344 logdivlti 14387 binom4 14482 lgsval2lem 14496 lgsval4a 14508 lgsneg1 14511 lgsdilem 14513 lgsdir2lem4 14517 lgsdir2 14519 lgsdir 14521 lgsmulsqcoprm 14532 lgsdirnn0 14533 lgsdinn0 14534 2sqlem8 14555 qdencn 14860 |
Copyright terms: Public domain | W3C validator |