Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulcl | GIF version |
Description: Alias for ax-mulcl 6982, for naming consistency with mulcli 7032. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcl 6982 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 · cmul 6894 |
This theorem was proved from axioms: ax-mulcl 6982 |
This theorem is referenced by: 0cn 7019 mulid1 7024 mulcli 7032 mulcld 7047 mul31 7144 mul4 7145 cnegexlem2 7187 cnegex 7189 muladd 7381 subdi 7382 mul02 7384 submul2 7396 mulsub 7398 recextlem1 7632 recexap 7634 muleqadd 7649 divassap 7669 divmuldivap 7688 divmuleqap 7693 divadddivap 7703 conjmulap 7705 cju 7913 zneo 8339 expivallem 9256 expival 9257 exp1 9261 expp1 9262 expcl 9273 expclzaplem 9279 mulexp 9294 sqcl 9315 subsq 9358 subsq2 9359 binom2sub 9364 binom3 9366 zesq 9367 bernneq 9369 bernneq2 9370 reim 9452 imcl 9454 crre 9457 crim 9458 remim 9460 mulreap 9464 cjreb 9466 recj 9467 reneg 9468 readd 9469 remullem 9471 remul2 9473 imcj 9475 imneg 9476 imadd 9477 immul2 9480 cjadd 9484 ipcnval 9486 cjmulrcl 9487 cjneg 9490 imval2 9494 cjreim 9503 rennim 9600 sqabsadd 9653 sqabssub 9654 absreimsq 9665 absreim 9666 absmul 9667 mulcn2 9833 climmul 9847 iisermulc2 9860 |
Copyright terms: Public domain | W3C validator |