![]() |
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 7623 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1184 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-mulass 7598 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: ltmul1 8220 recexap 8275 mulap0 8276 mulcanapd 8283 receuap 8291 divmulasscomap 8317 divdivdivap 8334 divmuleqap 8338 conjmulap 8350 apmul1 8409 qapne 9281 modqmul1 9991 modqdi 10006 expadd 10176 mulbinom2 10249 binom3 10250 faclbnd 10328 faclbnd6 10331 bcm1k 10347 bcp1nk 10349 bcval5 10350 crre 10470 remullem 10484 resqrexlemcalc1 10626 resqrexlemnm 10630 amgm2 10730 binomlem 11091 geo2sum 11122 mertenslemi1 11143 sinadd 11241 tanaddap 11244 dvdsmulcr 11318 dvdsmulgcd 11506 qredeq 11570 2sqpwodd 11646 |
Copyright terms: Public domain | W3C validator |