Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > remulcl | Unicode version |
Description: Alias for ax-mulrcl 6983, for naming consistency with remulcli 7041. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
remulcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulrcl 6983 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wcel 1393 (class class class)co 5512 cr 6888 cmul 6894 |
This theorem was proved from axioms: ax-mulrcl 6983 |
This theorem is referenced by: remulcli 7041 remulcld 7056 axmulgt0 7091 msqge0 7607 mulge0 7610 recexaplem2 7633 recexap 7634 ltmul12a 7826 lemul12b 7827 mulgt1 7829 ltdivmul 7842 cju 7913 addltmul 8161 zmulcl 8297 irrmul 8581 rpmulcl 8607 ge0mulcl 8851 iccdil 8866 reexpcl 9272 reexpclzap 9275 expge0 9291 expge1 9292 expubnd 9311 bernneq 9369 crre 9457 remim 9460 mulreap 9464 amgm2 9714 |
Copyright terms: Public domain | W3C validator |