![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > addcomli | Structured version Visualization version Unicode version |
Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
mul.1 |
![]() ![]() ![]() ![]() |
mul.2 |
![]() ![]() ![]() ![]() |
addcomli.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
addcomli |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mul.2 |
. . 3
![]() ![]() ![]() ![]() | |
2 | mul.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | addcomi 9850 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | addcomli.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtri 2484 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4417 df-opab 4476 df-mpt 4477 df-id 4768 df-po 4774 df-so 4775 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-ov 6318 df-er 7389 df-en 7596 df-dom 7597 df-sdom 7598 df-pnf 9703 df-mnf 9704 df-ltxr 9706 |
This theorem is referenced by: mvlladdi 9918 negsubdi2i 9987 1p2e3 10763 4t4e16 11153 6t3e18 11158 6t5e30 11160 7t3e21 11163 7t4e28 11164 7t6e42 11166 7t7e49 11167 8t3e24 11169 8t4e32 11170 8t5e40 11171 8t8e64 11174 9t3e27 11176 9t4e36 11177 9t5e45 11178 9t6e54 11179 9t7e63 11180 9t8e72 11181 9t9e81 11182 4bc3eq4 12545 bpoly4 14161 bitsfzo 14458 gcdaddmlem 14541 6gcd4e2 14551 gcdi 15094 2exp8 15109 2exp16 15110 37prm 15141 43prm 15142 83prm 15143 139prm 15144 163prm 15145 317prm 15146 631prm 15147 1259lem1 15151 1259lem2 15152 1259lem3 15153 1259lem4 15154 1259lem5 15155 1259prm 15156 2503lem1 15157 2503lem2 15158 2503lem3 15159 2503prm 15160 4001lem1 15161 4001lem2 15162 4001lem4 15164 4001prm 15165 iaa 23330 dvradcnv 23425 eulerid 23478 binom4 23825 log2ublem3 23923 log2ub 23924 lgsdir2lem1 24300 m1lgs 24339 ex-ind-dvds 25948 vcm 26239 fib5 29287 fib6 29288 inductionexd 36638 lhe4.4ex1a 36722 dirkertrigeqlem1 37998 sqwvfoura 38130 sqwvfourb 38131 fourierswlem 38132 fouriersw 38133 gbpart8 38907 |
Copyright terms: Public domain | W3C validator |