![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcomd | GIF version |
Description: Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
mulcomd | ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | mulcom 7673 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | |
4 | 1, 2, 3 | syl2anc 406 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1314 ∈ wcel 1463 (class class class)co 5728 ℂcc 7545 · cmul 7552 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 ax-mulcom 7646 |
This theorem is referenced by: mul31 7816 remulext2 8280 mulreim 8284 mulext2 8293 mulcanapd 8335 mulcanap2d 8336 divcanap1 8354 divrecap2 8362 div23ap 8364 divdivdivap 8386 divmuleqap 8390 divadddivap 8400 apmul2 8462 apdivmuld 8486 divcanap5rd 8491 dmdcanap2d 8494 mvllmulapd 8511 prodgt0 8520 lt2mul2div 8547 mulle0r 8612 qapne 9333 modqvalr 9991 modqcyc 10025 mulp1mod1 10031 modqmul12d 10044 modqnegd 10045 modqmulmodr 10056 addmodlteq 10064 expaddzap 10230 binom2 10296 binom3 10302 bccmpl 10393 bcm1k 10399 bcn2 10403 bcpasc 10405 cvg1nlemcxze 10646 cvg1nlemcau 10648 resqrexlemcalc1 10678 resqrexlemcalc2 10679 resqrexlemnm 10682 recvalap 10761 bdtrilem 10902 reccn2ap 10974 isummulc1 11088 fsummulc1 11110 trireciplem 11161 geolim 11172 cvgratnnlemnexp 11185 cvgratnnlemmn 11186 cvgratnnlemfm 11190 cvgratz 11193 mertensabs 11198 eftlub 11247 sinadd 11294 cosadd 11295 sin2t 11307 nndivides 11348 dvds2ln 11374 even2n 11419 oddm1even 11420 m1exp1 11446 divalgmod 11472 mulgcdr 11552 rplpwr 11561 lcmgcdlem 11604 divgcdcoprmex 11629 cncongr1 11630 oddpwdclemxy 11692 2sqpwodd 11699 evenennn 11751 dvmulxxbr 12621 |
Copyright terms: Public domain | W3C validator |