![]() |
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 8107 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | |
4 | 1, 2, 3 | syl2anc 411 | 1 ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1363 ∈ wcel 2158 (class class class)co 5888 ℂcc 7822 + caddc 7827 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-addcom 7924 |
This theorem is referenced by: muladd11r 8126 comraddd 8127 subadd2 8174 pncan 8176 npcan 8179 subcan 8225 mvlladdd 8335 subaddeqd 8339 addrsub 8341 ltadd1 8399 leadd2 8401 ltsubadd2 8403 lesubadd2 8405 mulreim 8574 apadd2 8579 recp1lt1 8869 ltaddrp2d 9744 lincmb01cmp 10016 iccf1o 10017 rebtwn2zlemstep 10266 qavgle 10272 modqaddabs 10375 mulqaddmodid 10377 qnegmod 10382 modqadd2mod 10387 modqadd12d 10393 modqaddmulmod 10404 addmodlteq 10411 expaddzap 10577 bcn2m1 10762 bcn2p1 10763 remullem 10893 resqrexlemover 11032 maxabslemab 11228 maxabslemval 11230 bdtrilem 11260 climaddc2 11351 telfsumo 11487 fsumparts 11491 bcxmas 11510 isumshft 11511 cvgratnnlemsumlt 11549 cosneg 11748 sinadd 11757 sincossq 11769 cos2t 11771 absefi 11789 absefib 11791 gcdaddm 11998 pythagtrip 12296 mulgnndir 13043 mulgdirlem 13045 metrtri 14148 lgseisenlem1 14721 2sqlem3 14735 apdifflemf 15066 apdiff 15068 |
Copyright terms: Public domain | W3C validator |