![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcom | GIF version |
Description: Alias for ax-mulcom 7911, for naming consistency with mulcomi 7962. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 7911 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1353 ∈ wcel 2148 (class class class)co 5874 ℂcc 7808 · cmul 7815 |
This theorem was proved from axioms: ax-mulcom 7911 |
This theorem is referenced by: adddir 7947 mullid 7954 mulcomi 7962 mulcomd 7978 mul12 8085 mul32 8086 mul31 8087 muladd 8340 subdir 8342 mul01 8345 mulneg2 8352 recextlem1 8607 divmulap3 8633 div23ap 8647 div13ap 8649 div12ap 8650 divmulasscomap 8652 divcanap4 8655 divmul13ap 8671 divmul24ap 8672 divcanap7 8677 div2negap 8691 prodgt02 8809 prodge02 8811 ltmul2 8812 lemul2 8813 lemul2a 8815 ltmulgt12 8821 lemulge12 8823 ltmuldiv2 8831 ltdivmul2 8834 ledivmul2 8836 lemuldiv2 8838 times2 9047 modqcyc2 10359 subsq 10626 cjmulrcl 10895 imval2 10902 abscj 11060 sqabsadd 11063 sqabssub 11064 prod3fmul 11548 prodmodclem3 11582 efcllemp 11665 efexp 11689 sinmul 11751 demoivreALT 11780 dvdsmul1 11819 odd2np1lem 11876 odd2np1 11877 opeo 11901 omeo 11902 modgcd 11991 dvdsgcd 12012 gcdmultiple 12020 coprmdvds 12091 coprmdvds2 12092 qredeq 12095 modprm0 12253 modprmn0modprm0 12255 coprimeprodsq2 12257 cncrng 13399 ef2kpi 14163 sinperlem 14165 sinmpi 14172 cosmpi 14173 sinppi 14174 cosppi 14175 cxpcom 14293 lgsdir2lem4 14368 lgsdir2 14370 |
Copyright terms: Public domain | W3C validator |