![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcld | Unicode version |
Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
addcld.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mulcld |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | addcld.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | mulcl 7214 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 403 |
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-ia3 106 ax-mulcl 7188 |
This theorem is referenced by: kcnktkm1cn 7606 rereim 7805 cru 7821 apreim 7822 mulreim 7823 apadd1 7827 apneg 7830 mulext1 7831 mulext 7833 mulap0 7863 receuap 7878 divrecap 7895 divcanap3 7905 muldivdirap 7914 divdivdivap 7920 divsubdivap 7935 apmul1 7995 qapne 8857 cnref1o 8866 lincmb01cmp 9153 iccf1o 9154 qbtwnrelemcalc 9394 flqpmodeq 9461 modq0 9463 modqdiffl 9469 modqvalp1 9477 modqcyc 9493 modqcyc2 9494 modqadd1 9495 mulqaddmodid 9498 modqmuladdnn0 9502 qnegmod 9503 modqmul1 9511 mulexpzap 9665 expmulzap 9671 binom2 9734 binom3 9739 bernneq 9742 nn0opthd 9798 ibcval5 9839 remullem 9959 cjreim2 9992 cnrecnv 9998 absval 10088 resqrexlemover 10097 resqrexlemcalc1 10101 resqrexlemnm 10105 absimle 10171 abstri 10191 mulcn2 10352 iisermulc2 10379 climcvg1nlem 10387 dvdscmulr 10432 dvdsmulcr 10433 dvds2ln 10436 oddm1even 10482 divalglemnn 10525 divalglemnqt 10527 flodddiv4 10541 gcdaddm 10582 bezoutlemnewy 10592 bezoutlema 10595 bezoutlemb 10596 lcmgcdlem 10666 oddpwdc 10759 phiprmpw 10805 oddennn 10812 qdencn 11052 |
Copyright terms: Public domain | W3C validator |