![]() |
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 | ⊢ (φ → A ∈ ℂ) |
addcld.2 | ⊢ (φ → B ∈ ℂ) |
Ref | Expression |
---|---|
mulcomd | ⊢ (φ → (A · B) = (B · A)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (φ → A ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (φ → B ∈ ℂ) | |
3 | mulcom 6808 | . 2 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) = (B · A)) | |
4 | 1, 2, 3 | syl2anc 391 | 1 ⊢ (φ → (A · B) = (B · A)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1242 ∈ wcel 1390 (class class class)co 5455 ℂcc 6709 · cmul 6716 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 ax-mulcom 6784 |
This theorem is referenced by: mul31 6941 remulext2 7384 mulreim 7388 mulext2 7397 mulcanapd 7424 mulcanap2d 7425 divcanap1 7442 divrecap2 7450 div23ap 7452 divdivdivap 7471 divmuleqap 7475 divadddivap 7485 divcanap5rd 7574 dmdcanap2d 7577 mvllmulapd 7590 prodgt0 7599 lt2mul2div 7626 qapne 8350 expaddzap 8953 binom2 9015 binom3 9019 |
Copyright terms: Public domain | W3C validator |