Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulass | Unicode version |
Description: Alias for ax-mulass 7847, for naming consistency with mulassi 7899. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulass |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulass 7847 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 967 wceq 1342 wcel 2135 (class class class)co 5836 cc 7742 cmul 7749 |
This theorem was proved from axioms: ax-mulass 7847 |
This theorem is referenced by: mulid1 7887 mulassi 7899 mulassd 7913 mul12 8018 mul32 8019 mul31 8020 mul4 8021 rimul 8474 divassap 8577 cju 8847 div4p1lem1div2 9101 mulbinom2 10560 sqoddm1div8 10597 remim 10788 imval2 10822 clim2divap 11467 prod3fmul 11468 prodmodclem3 11502 absefib 11697 efieq1re 11698 muldvds1 11742 muldvds2 11743 dvdsmulc 11745 dvdstr 11754 oddprmdvds 12263 abssinper 13314 |
Copyright terms: Public domain | W3C validator |