![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pncan | Unicode version |
Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
pncan |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 461 | . . 3 | |
2 | simpl 457 | . . 3 | |
3 | 1, 2 | addcomd 9803 | . 2 |
4 | addcl 9595 | . . 3 | |
5 | subadd 9846 | . . 3 | |
6 | 4, 1, 2, 5 | syl3anc 1228 | . 2 |
7 | 3, 6 | mpbird 232 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
/\ wa 369 = wceq 1395 e. wcel 1818
(class class class)co 6296 cc 9511 caddc 9516 cmin 9828 |
This theorem is referenced by: pncan2 9850 addsubass 9853 pncan3oi 9859 subid1 9862 nppcan2 9873 pncand 9955 nn1m1nn 10581 nnsub 10599 elnn0nn 10863 elz2 10906 zrevaddcl 10934 uzindOLD 10982 qrevaddcl 11233 irradd 11235 fzrev3 11774 elfzp1b 11784 fzrevral3 11794 fzval3 11885 seqf1olem1 12146 seqf1olem2 12147 subsq2 12276 bcp1nk 12395 bcp1m1 12398 bcpasc 12399 hashbclem 12501 wrdind 12702 wrd2ind 12703 2cshwcshw 12793 shftlem 12901 shftval5 12911 isershft 13486 isercoll2 13491 fsump1 13571 mptfzshft 13593 telfsumo 13616 fsumparts 13620 bcxmas 13647 isum1p 13653 geolim 13679 mertenslem2 13694 mertens 13695 eftlub 13844 effsumlt 13846 eirrlem 13937 dvdsadd 14024 prmind2 14228 iserodd 14359 fldivp1 14416 prmpwdvds 14422 pockthlem 14423 prmreclem4 14437 prmreclem6 14439 4sqlem11 14473 vdwapun 14492 ramub1lem1 14544 ramcl 14547 efgsval2 16751 efgsrel 16752 pcoass 21524 shft2rab 21919 uniioombllem3 21994 uniioombllem4 21995 dvexp 22356 dvfsumlem1 22427 degltp1le 22473 ply1divex 22537 plyaddlem1 22610 plymullem1 22611 dvply1 22680 dvply2g 22681 vieta1lem2 22707 aaliou3lem7 22745 dvradcnv 22816 pserdvlem2 22823 abssinper 22911 advlogexp 23036 atantayl3 23270 leibpilem1 23271 leibpilem2 23272 emcllem2 23326 harmonicbnd4 23340 wilthlem2 23343 basellem8 23361 ppiprm 23425 ppinprm 23426 chtprm 23427 chtnprm 23428 chpp1 23429 chtub 23487 perfectlem1 23504 perfectlem2 23505 perfect 23506 bcp1ctr 23554 lgsvalmod 23590 lgseisen 23628 lgsquadlem1 23629 lgsquad2lem1 23633 2sqlem10 23649 rplogsumlem1 23669 selberg2lem 23735 logdivbnd 23741 pntrsumo1 23750 pntpbnd2 23772 wlklenvm1 24532 wlkiswwlk1 24690 wwlknext 24724 clwwlkf1 24796 eupap1 24976 eupath2lem3 24979 extwwlkfablem2 25078 gxadd 25277 subfacp1lem5 28628 subfacp1lem6 28629 subfacval2 28631 subfaclim 28632 cvmliftlem7 28736 cvmliftlem10 28739 fsumkthpow 29818 mblfinlem2 30052 itg2addnclem3 30068 fdc 30238 mettrifi 30250 heiborlem4 30310 heiborlem6 30312 lzenom 30703 2nn0ind 30881 jm2.17a 30898 jm2.17b 30899 jm2.17c 30900 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-8 1820 ax-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-sep 4573 ax-nul 4581 ax-pow 4630 ax-pr 4691 ax-un 6592 ax-resscn 9570 ax-1cn 9571 ax-icn 9572 ax-addcl 9573 ax-addrcl 9574 ax-mulcl 9575 ax-mulrcl 9576 ax-mulcom 9577 ax-addass 9578 ax-mulass 9579 ax-distr 9580 ax-i2m1 9581 ax-1ne0 9582 ax-1rid 9583 ax-rnegex 9584 ax-rrecex 9585 ax-cnre 9586 ax-pre-lttri 9587 ax-pre-lttrn 9588 ax-pre-ltadd 9589 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-eu 2286 df-mo 2287 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3435 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-nul 3785 df-if 3942 df-pw 4014 df-sn 4030 df-pr 4032 df-op 4036 df-uni 4250 df-br 4453 df-opab 4511 df-mpt 4512 df-id 4800 df-po 4805 df-so 4806 df-xp 5010 df-rel 5011 df-cnv 5012 df-co 5013 df-dm 5014 df-rn 5015 df-res 5016 df-ima 5017 df-iota 5556 df-fun 5595 df-fn 5596 df-f 5597 df-f1 5598 df-fo 5599 df-f1o 5600 df-fv 5601 df-riota 6257 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-er 7330 df-en 7537 df-dom 7538 df-sdom 7539 df-pnf 9651 df-mnf 9652 df-ltxr 9654 df-sub 9830 |
Copyright terms: Public domain | W3C validator |