Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulassd | Unicode version |
Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | |
addcld.2 | |
addassd.3 |
Ref | Expression |
---|---|
mulassd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 | |
2 | addcld.2 | . 2 | |
3 | addassd.3 | . 2 | |
4 | mulass 7898 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1233 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1348 wcel 2141 (class class class)co 5851 cc 7765 cmul 7772 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-mulass 7870 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: ltmul1 8504 recexap 8564 mulap0 8565 mulcanapd 8572 receuap 8580 divmulasscomap 8606 divdivdivap 8623 divmuleqap 8627 conjmulap 8639 apmul1 8698 qapne 9591 modqmul1 10326 modqdi 10341 expadd 10511 mulbinom2 10585 binom3 10586 faclbnd 10668 faclbnd6 10671 bcm1k 10687 bcp1nk 10689 bcval5 10690 crre 10814 remullem 10828 resqrexlemcalc1 10971 resqrexlemnm 10975 amgm2 11075 binomlem 11439 geo2sum 11470 mertenslemi1 11491 clim2prod 11495 sinadd 11692 tanaddap 11695 dvdsmulcr 11776 dvdsmulgcd 11973 qredeq 12043 2sqpwodd 12123 pcaddlem 12285 prmpwdvds 12300 dvexp 13434 tangtx 13518 cxpmul 13592 binom4 13656 lgsneg 13684 2sqlem3 13712 |
Copyright terms: Public domain | W3C validator |