![]() |
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 8003 | . 2 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (1 · 𝐴) = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 ∈ wcel 2160 (class class class)co 5906 ℂcc 7856 1c1 7859 · cmul 7863 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-resscn 7950 ax-1cn 7951 ax-icn 7953 ax-addcl 7954 ax-mulcl 7956 ax-mulcom 7959 ax-mulass 7961 ax-distr 7962 ax-1rid 7965 ax-cnre 7969 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-v 2758 df-un 3153 df-in 3155 df-ss 3162 df-sn 3620 df-pr 3621 df-op 3623 df-uni 3832 df-br 4026 df-iota 5203 df-fv 5250 df-ov 5909 |
This theorem is referenced by: adddirp1d 8032 mulsubfacd 8423 mulcanapd 8666 receuap 8674 divdivdivap 8718 divcanap5 8719 subrecap 8844 ltrec 8888 recp1lt1 8904 nndivtr 9010 xp1d2m1eqxm1d2 9221 gtndiv 9398 lincmb01cmp 10055 iccf1o 10056 modqfrac 10394 qnegmod 10426 addmodid 10429 m1expcl2 10606 expgt1 10622 ltexp2a 10636 leexp2a 10637 binom3 10702 faclbnd 10786 facavg 10791 bcval5 10808 cvg1nlemcau 11102 resqrexlemover 11128 resqrexlemcalc2 11133 absimle 11202 maxabslemlub 11325 reccn2ap 11430 binom1p 11602 binom1dif 11604 fprodsplitdc 11713 fprodcl2lem 11722 efcllemp 11775 ef01bndlem 11873 efieq1re 11889 eirraplem 11894 iddvds 11921 gcdaddm 12095 rpmulgcd 12137 prmind2 12232 isprm5lem 12253 phiprm 12335 eulerthlemth 12344 fermltl 12346 hashgcdlem 12350 odzdvds 12357 powm2modprm 12364 modprm0 12366 pythagtriplem4 12380 mulgnnass 13201 dvexp 14817 dvef 14830 reeff1oleme 14835 sin0pilem1 14844 sinhalfpip 14883 sinhalfpim 14884 coshalfpip 14885 coshalfpim 14886 tangtx 14901 logdivlti 14944 binom4 15039 lgsval2lem 15054 lgsval4a 15066 lgsneg1 15069 lgsdilem 15071 lgsdir2lem4 15075 lgsdir2 15077 lgsdir 15079 lgsmulsqcoprm 15090 lgsdirnn0 15091 lgsdinn0 15092 2sqlem8 15134 qdencn 15441 |
Copyright terms: Public domain | W3C validator |