![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addcomd | GIF version |
Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcomd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
addcomd | ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcomd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addcom 7680 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | |
4 | 1, 2, 3 | syl2anc 404 | 1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1290 ∈ wcel 1439 (class class class)co 5666 ℂcc 7409 + caddc 7414 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 ax-addcom 7506 |
This theorem is referenced by: muladd11r 7699 comraddd 7700 subadd2 7747 pncan 7749 npcan 7752 subcan 7798 subaddeqd 7908 addrsub 7910 ltadd1 7968 leadd2 7970 ltsubadd2 7972 lesubadd2 7974 mulreim 8142 apadd2 8147 recp1lt1 8421 ltaddrp2d 9269 lincmb01cmp 9481 iccf1o 9482 rebtwn2zlemstep 9725 qavgle 9731 modqaddabs 9830 mulqaddmodid 9832 qnegmod 9837 modqadd2mod 9842 modqadd12d 9848 modqaddmulmod 9859 addmodlteq 9866 expaddzap 10060 bcn2m1 10238 bcn2p1 10239 remullem 10366 resqrexlemover 10504 maxabslemab 10700 maxabslemval 10702 climaddc2 10779 telfsumo 10921 fsumparts 10925 bcxmas 10944 isumshft 10945 cvgratnnlemsumlt 10983 cosneg 11079 sinadd 11088 sincossq 11100 cos2t 11102 absefi 11119 absefib 11121 gcdaddm 11314 |
Copyright terms: Public domain | W3C validator |