![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subaddd | Structured version Visualization version Unicode version |
Description: Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
negidd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pncand.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
subaddd.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
subaddd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pncand.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | subaddd.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | subadd 9883 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1269 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-mpt 4466 df-id 4752 df-po 4758 df-so 4759 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-pnf 9682 df-mnf 9683 df-ltxr 9685 df-sub 9867 |
This theorem is referenced by: addid0 10046 subdi 10059 zneo 11025 flpmodeq 12108 cvgcmpce 13890 bpolysum 14118 sin01bnd 14251 cos01bnd 14252 phiprmpw 14736 fldivp1 14854 pcfac 14856 sylow2a 17283 dveflem 22943 aaliou3lem7 23317 mtest 23371 efiarg 23568 quad2 23777 dcubic 23784 quart 23799 efiatan2 23855 dmgmaddn0 23960 lgamgulmlem3 23968 m1lgs 24302 logdivbnd 24406 colinearalglem2 24949 axeuclidlem 25004 ballotlemic 29351 ballotlemicOLD 29389 signslema 29463 signsvtn 29485 subfaclim 29923 mblfinlem3 31991 mblfinlem4 31992 pell1qrge1 35728 rmxluc 35796 itgsinexp 37841 fourierdlem19 37998 fourierdlem35 38015 fourierdlem41 38021 fourierdlem51 38031 fourierdlem79 38059 nnpw2pmod 40498 |
Copyright terms: Public domain | W3C validator |