| 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 8059 |
. 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 8030 |
| This theorem is referenced by: ixi 8663 2mulicn 9266 numma 9554 nummac 9555 9t11e99 9640 decbin2 9651 irec 10791 binom2i 10800 3dec 10866 rei 11254 imi 11255 3dvdsdec 12220 3dvds2dec 12221 odd2np1 12228 3lcm2e6woprm 12452 6lcm4e12 12453 modxai 12783 karatsuba 12797 sinhalfpilem 15307 ef2pi 15321 ef2kpi 15322 efper 15323 sinperlem 15324 sin2kpi 15327 cos2kpi 15328 sin2pim 15329 cos2pim 15330 sincos4thpi 15356 sincos6thpi 15358 abssinper 15362 cosq34lt1 15366 lgsdir2lem5 15553 2lgsoddprmlem3c 15630 2lgsoddprmlem3d 15631 |
| Copyright terms: Public domain | W3C validator |