| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > mulridd | Unicode version | ||
| Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
| Ref | Expression |
|---|---|
| addcld.1 |
|
| Ref | Expression |
|---|---|
| mulridd |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | addcld.1 |
. 2
| |
| 2 | mulrid 8068 |
. 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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 ax-resscn 8016 ax-1cn 8017 ax-icn 8019 ax-addcl 8020 ax-mulcl 8022 ax-mulcom 8025 ax-mulass 8027 ax-distr 8028 ax-1rid 8031 ax-cnre 8035 |
| This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ral 2488 df-rex 2489 df-v 2773 df-un 3169 df-in 3171 df-ss 3178 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-br 4044 df-iota 5231 df-fv 5278 df-ov 5946 |
| This theorem is referenced by: muladd11 8204 muls1d 8489 ltmul1 8664 mulap0 8726 divrecap 8760 diveqap1 8777 conjmulap 8801 apmul1 8860 qapne 9759 divelunit 10123 modqid 10492 q2submod 10528 addmodlteq 10541 expadd 10724 leexp2r 10736 nnlesq 10786 sqoddm1div8 10836 nn0opthlem1d 10863 faclbnd 10884 faclbnd2 10885 faclbnd6 10887 facavg 10889 bcn0 10898 bcn1 10901 reccn2ap 11595 hash2iun1dif1 11762 binom11 11768 trireciplem 11782 geosergap 11788 cvgratnnlemnexp 11806 cvgratnnlemmn 11807 fprodsplitdc 11878 efzval 11965 tanaddaplem 12020 tanaddap 12021 cos01gt0 12045 absef 12052 1dvds 12087 bitsfzo 12237 bitsmod 12238 bezoutlema 12291 bezoutlemb 12292 gcdmultiple 12312 sqgcd 12321 lcm1 12374 coprmdvds 12385 qredeu 12390 phiprmpw 12515 coprimeprodsq 12551 pc2dvds 12624 sumhashdc 12641 fldivp1 12642 pcfaclem 12643 prmpwdvds 12649 zsssubrg 14318 mulgrhm2 14343 znrrg 14393 dveflem 15169 plyconst 15188 plycolemc 15201 efper 15250 tangtx 15281 logdivlti 15324 rpcxpmul2 15356 relogbexpap 15401 rplogbcxp 15406 0sgm 15428 lgsdir2 15481 lgsquad2lem1 15529 lgsquad3 15532 2sqlem6 15568 2sqlem8 15571 trilpolemclim 15937 trilpolemisumle 15939 trilpolemeq1 15941 trilpolemlt1 15942 redcwlpolemeq1 15955 nconstwlpolemgt0 15965 |
| Copyright terms: Public domain | W3C validator |