![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcli | Unicode version |
Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 |
![]() ![]() ![]() ![]() |
axi.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mulcli |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | axi.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | mulcl 7973 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 426 |
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-ia3 108 ax-mulcl 7944 |
This theorem is referenced by: ixi 8575 2mulicn 9176 numma 9462 nummac 9463 9t11e99 9548 decbin2 9559 irec 10660 binom2i 10669 3dec 10735 rei 10949 imi 10950 3dvdsdec 11911 3dvds2dec 11912 odd2np1 11919 3lcm2e6woprm 12129 6lcm4e12 12130 sinhalfpilem 14697 ef2pi 14711 ef2kpi 14712 efper 14713 sinperlem 14714 sin2kpi 14717 cos2kpi 14718 sin2pim 14719 cos2pim 14720 sincos4thpi 14746 sincos6thpi 14748 abssinper 14752 cosq34lt1 14756 lgsdir2lem5 14919 2lgsoddprmlem3c 14943 2lgsoddprmlem3d 14944 |
Copyright terms: Public domain | W3C validator |