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 7715 | . 2 | |
4 | 1, 2, 3 | mp2an 422 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1465 (class class class)co 5742 cc 7586 cmul 7593 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-mulcl 7686 |
This theorem is referenced by: ixi 8313 2mulicn 8910 numma 9193 nummac 9194 9t11e99 9279 decbin2 9290 irec 10360 binom2i 10369 3dec 10429 rei 10639 imi 10640 3dvdsdec 11489 3dvds2dec 11490 odd2np1 11497 3lcm2e6woprm 11694 6lcm4e12 11695 sinhalfpilem 12799 ef2pi 12813 ef2kpi 12814 efper 12815 sinperlem 12816 sin2kpi 12819 cos2kpi 12820 sin2pim 12821 cos2pim 12822 sincos4thpi 12848 sincos6thpi 12850 abssinper 12854 cosq34lt1 12858 |
Copyright terms: Public domain | W3C validator |