Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulcom | GIF version |
Description: Alias for ax-mulcom 7828, for naming consistency with mulcomi 7879. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 7828 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1335 ∈ wcel 2128 (class class class)co 5821 ℂcc 7725 · cmul 7732 |
This theorem was proved from axioms: ax-mulcom 7828 |
This theorem is referenced by: adddir 7864 mulid2 7871 mulcomi 7879 mulcomd 7894 mul12 7999 mul32 8000 mul31 8001 muladd 8254 subdir 8256 mul01 8259 mulneg2 8266 recextlem1 8520 divmulap3 8545 div23ap 8559 div13ap 8561 div12ap 8562 divmulasscomap 8564 divcanap4 8567 divmul13ap 8583 divmul24ap 8584 divcanap7 8589 div2negap 8603 prodgt02 8719 prodge02 8721 ltmul2 8722 lemul2 8723 lemul2a 8725 ltmulgt12 8731 lemulge12 8733 ltmuldiv2 8741 ltdivmul2 8744 ledivmul2 8746 lemuldiv2 8748 times2 8957 modqcyc2 10254 subsq 10520 cjmulrcl 10782 imval2 10789 abscj 10947 sqabsadd 10950 sqabssub 10951 prod3fmul 11433 prodmodclem3 11467 efcllemp 11550 efexp 11574 sinmul 11636 demoivreALT 11665 dvdsmul1 11703 odd2np1lem 11757 odd2np1 11758 opeo 11782 omeo 11783 modgcd 11869 dvdsgcd 11890 gcdmultiple 11898 coprmdvds 11963 coprmdvds2 11964 qredeq 11967 ef2kpi 13114 sinperlem 13116 sinmpi 13123 cosmpi 13124 sinppi 13125 cosppi 13126 cxpcom 13244 |
Copyright terms: Public domain | W3C validator |