Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulcom | GIF version |
Description: Alias for ax-mulcom 6985, for naming consistency with mulcomi 7033. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 6985 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 = wceq 1243 ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 · cmul 6894 |
This theorem was proved from axioms: ax-mulcom 6985 |
This theorem is referenced by: adddir 7018 mulid2 7025 mulcomi 7033 mulcomd 7048 mul12 7142 mul32 7143 mul31 7144 muladd 7381 subdir 7383 mul01 7386 mulneg2 7393 recextlem1 7632 divmulap3 7656 div23ap 7670 div13ap 7672 div12ap 7673 divcanap4 7676 divmul13ap 7691 divmul24ap 7692 divcanap7 7697 div2negap 7711 prodgt02 7819 prodge02 7821 ltmul2 7822 lemul2 7823 lemul2a 7825 ltmulgt12 7831 lemulge12 7833 ltmuldiv2 7841 ltdivmul2 7844 ledivmul2 7846 lemuldiv2 7848 times2 8039 subsq 9358 cjmulrcl 9487 imval2 9494 abscj 9650 sqabsadd 9653 sqabssub 9654 |
Copyright terms: Public domain | W3C validator |