![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulid2d | Unicode version |
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mulid2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mullid 7990 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
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 7938 ax-1cn 7939 ax-icn 7941 ax-addcl 7942 ax-mulcl 7944 ax-mulcom 7947 ax-mulass 7949 ax-distr 7950 ax-1rid 7953 ax-cnre 7957 |
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 2754 df-un 3148 df-in 3150 df-ss 3157 df-sn 3616 df-pr 3617 df-op 3619 df-uni 3828 df-br 4022 df-iota 5199 df-fv 5246 df-ov 5903 |
This theorem is referenced by: adddirp1d 8019 mulsubfacd 8410 mulcanapd 8653 receuap 8661 divdivdivap 8705 divcanap5 8706 subrecap 8831 ltrec 8875 recp1lt1 8891 nndivtr 8996 xp1d2m1eqxm1d2 9206 gtndiv 9383 lincmb01cmp 10039 iccf1o 10040 modqfrac 10374 qnegmod 10406 addmodid 10409 m1expcl2 10582 expgt1 10598 ltexp2a 10612 leexp2a 10613 binom3 10678 faclbnd 10762 facavg 10767 bcval5 10784 cvg1nlemcau 11034 resqrexlemover 11060 resqrexlemcalc2 11065 absimle 11134 maxabslemlub 11257 reccn2ap 11362 binom1p 11534 binom1dif 11536 fprodsplitdc 11645 fprodcl2lem 11654 efcllemp 11707 ef01bndlem 11805 efieq1re 11820 eirraplem 11825 iddvds 11852 gcdaddm 12026 rpmulgcd 12068 prmind2 12163 isprm5lem 12184 phiprm 12266 eulerthlemth 12275 fermltl 12277 hashgcdlem 12281 odzdvds 12288 powm2modprm 12295 modprm0 12297 pythagtriplem4 12311 mulgnnass 13122 dvexp 14660 dvef 14673 reeff1oleme 14678 sin0pilem1 14687 sinhalfpip 14726 sinhalfpim 14727 coshalfpip 14728 coshalfpim 14729 tangtx 14744 logdivlti 14787 binom4 14882 lgsval2lem 14897 lgsval4a 14909 lgsneg1 14912 lgsdilem 14914 lgsdir2lem4 14918 lgsdir2 14920 lgsdir 14922 lgsmulsqcoprm 14933 lgsdirnn0 14934 lgsdinn0 14935 2sqlem8 14956 qdencn 15263 |
Copyright terms: Public domain | W3C validator |