![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulass | Unicode version |
Description: Alias for ax-mulass 7944, for naming consistency with mulassi 7996. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulass |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulass 7944 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulass 7944 |
This theorem is referenced by: mulrid 7984 mulassi 7996 mulassd 8011 mul12 8116 mul32 8117 mul31 8118 mul4 8119 rimul 8572 divassap 8677 cju 8948 div4p1lem1div2 9202 mulbinom2 10668 sqoddm1div8 10705 remim 10901 imval2 10935 clim2divap 11580 prod3fmul 11581 prodmodclem3 11615 absefib 11810 efieq1re 11811 muldvds1 11855 muldvds2 11856 dvdsmulc 11858 dvdstr 11867 oddprmdvds 12386 cncrng 13872 abssinper 14724 2sqlem6 14925 |
Copyright terms: Public domain | W3C validator |