![]() |
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 7967 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1249 |
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-mulass 7939 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: ltmul1 8574 recexap 8635 mulap0 8636 mulcanapd 8643 receuap 8651 divmulasscomap 8678 divdivdivap 8695 divmuleqap 8699 conjmulap 8711 apmul1 8770 qapne 9664 modqmul1 10403 modqdi 10418 expadd 10588 mulbinom2 10663 binom3 10664 faclbnd 10748 faclbnd6 10751 bcm1k 10767 bcp1nk 10769 bcval5 10770 crre 10893 remullem 10907 resqrexlemcalc1 11050 resqrexlemnm 11054 amgm2 11154 binomlem 11518 geo2sum 11549 mertenslemi1 11570 clim2prod 11574 sinadd 11771 tanaddap 11774 dvdsmulcr 11855 dvdsmulgcd 12053 qredeq 12123 2sqpwodd 12203 pcaddlem 12366 prmpwdvds 12382 dvexp 14612 tangtx 14696 cxpmul 14770 binom4 14834 lgsneg 14863 lgseisenlem1 14888 lgseisenlem2 14889 2lgsoddprmlem2 14892 2sqlem3 14902 |
Copyright terms: Public domain | W3C validator |