breqtrd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > breqtrd		Structured version Visualization version GIF version

Theorem breqtrd 5176

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

**Hypotheses**
Ref	Expression
breqtrd.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

**Assertion**
Ref	Expression
breqtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

**Proof of Theorem breqtrd**
Step	Hyp	Ref	Expression
1		breqtrd.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	breq2d 5162	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶))
4	1, 3	mpbid 231	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1533 class class class wbr 5150

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5151

This theorem is referenced by: breqtrrd 5178 breqtrid 5187 domunsn 9156 mapdom2 9177 phplem2 9237 phplem4OLD 9249 mapfien2 9438 wemaplem2 9576 infdifsn 9686 cantnff 9703 ttrclss 9749 rnttrcl 9751 infxpenlem 10042 infmap2 10247 ssfin4 10339 canthp1lem1 10681 nqereq 10964 ltexnq 11004 ltbtwnnq 11007 add20 11762 mullt0 11769 ltm1 12092 recgt0 12096 prodgt0 12097 ltmul1a 12099 mulge0b 12120 recp1lt1 12148 recreclt 12149 ledivp1 12152 ledivp1i 12175 ltdivp1i 12176 eluzmn 12865 ltaddrp2d 13088 mul2lt0bi 13118 prodge0rd 13119 xleadd1a 13270 xov1plusxeqvd 13513 fz01en 13567 fzonmapblen 13716 fladdz 13828 flhalf 13833 fldiv 13863 modsubdir 13943 fzen2 13972 serle 14060 ltexp2a 14168 leexp2a 14174 exple1 14178 expubnd 14179 bernneq 14229 expmulnbnd 14235 discr1 14239 discr 14240 faclbnd6 14296 hashfz 14424 hashfun 14434 seqcoll 14463 sqeqd 15151 01sqrexlem7 15233 sqrtge0 15242 sqrtneglem 15251 abslt 15299 absle 15300 abstri 15315 rlimge0 15563 reccn2 15579 climaddc2 15618 isercolllem1 15649 caucvgrlem 15657 summolem2a 15699 isumge0 15750 fsumle 15783 fsumlt 15784 o1fsum 15797 supcvg 15840 expcnv 15848 geolim 15854 geolim2 15855 georeclim 15856 geo2lim 15859 mertenslem1 15868 mertens 15870 prodmolem2a 15916 efcllem 16059 ef0lem 16060 efgt0 16085 eftlub 16091 eflt 16099 sinbnd 16162 cosbnd 16163 ef01bndlem 16166 sin01gt0 16172 cos01gt0 16173 sin02gt0 16174 eirrlem 16186 rpnnen2lem11 16206 rpnnen2lem12 16207 ruclem11 16222 dvdssub2 16283 dvdsadd2b 16288 dvdsexp 16310 3dvds 16313 opoe 16345 bitsfzolem 16414 bitsinv1lem 16421 bezoutlem4 16523 dvdsgcd 16525 dvdsmulgcd 16536 bezoutr1 16545 nn0seqcvgd 16546 rpmulgcd2 16632 qredeq 16633 rpdvds 16636 prmind2 16661 divdenle 16726 hashdvds 16749 phimullem 16753 eulerthlem2 16756 prmdiveq 16760 prmdivdiv 16761 pythagtriplem4 16793 pythagtriplem10 16794 pythagtriplem19 16807 iserodd 16809 pcpre1 16816 pcadd2 16864 qexpz 16875 expnprm 16876 oddprmdvds 16877 pockthlem 16879 prmreclem2 16891 prmreclem3 16892 4sqlem7 16918 4sqlem10 16921 4sqlem11 16929 4sqlem12 16930 4sqlem14 16932 4sqlem15 16933 4sqlem16 16934 0ram 16994 ffthiso 17923 latmlej12 18476 qusgrp 19146 pgpfi1 19555 sylow1lem4 19561 sylow1lem5 19562 odcau 19564 pgpfi 19565 pgpssslw 19574 sylow3lem4 19590 sylow3lem6 19592 efgsfo 19699 frgp0 19720 odadd1 19808 odadd2 19809 odadd 19810 gexexlem 19812 lt6abl 19855 gsumzsubmcl 19878 pwsgsum 19942 dprd2dlem1 20003 dprd2d2 20006 ablfacrplem 20027 ablfacrp 20028 ablfacrp2 20029 ablfac1b 20032 ablfac1eu 20035 pgpfac1lem3a 20038 ablfaclem2 20048 dvdsrid 20311 dvdsrtr 20312 dvdsrneg 20314 unitmulcl 20324 unitgrp 20327 unitnegcl 20341 subrguss 20531 subrgunit 20534 isdrng2 20643 abvsubtri 20720 fidomndrnglem 21265 gzrngunit 21371 prmirredlem 21403 znidomb 21500 frlmgsum 21711 psrbaglesupp 21862 psrbaglesuppOLD 21863 psdmul 22095 invrvald 22596 psmetsym 24234 psmettri 24235 mettri2 24265 xmetsym 24271 xmettri 24275 prdsxmetlem 24292 xblss2ps 24325 xblss2 24326 blhalf 24329 xmsge0 24387 ngptgp 24563 nrginvrcnlem 24626 nmoeq0 24671 cnmet 24706 blcvx 24732 opnreen 24765 metdcnlem 24770 metdstri 24785 metdsle 24786 metnrmlem1 24793 metnrmlem3 24795 lebnumlem1 24905 pi1inv 24997 cphnmf 25141 ipge0 25144 ipcau2 25180 tcphcphlem1 25181 csbren 25345 minveclem2 25372 minveclem3 25375 ovolssnul 25434 ovolctb 25437 ovolunnul 25447 ovoliunlem1 25449 ovoliun2 25453 ovoliunnul 25454 ioombl1lem4 25508 uniioombllem3 25532 uniioombllem4 25533 uniioombllem5 25534 uniioombl 25536 volcn 25553 vitalilem2 25556 vitalilem5 25559 itg1lea 25660 mbfi1fseqlem6 25668 mbfi1flimlem 25670 itg2eqa 25693 itg2splitlem 25696 itg2split 25697 itg2monolem1 25698 itg2cnlem2 25710 iblabsr 25777 iblmulc2 25778 bddiblnc 25789 dveflem 25929 dvef 25930 dvferm2lem 25936 dvlip 25944 c1liplem1 25947 dveq0 25951 dvlt0 25956 dvivthlem1 25959 lhop1 25965 dvfsumle 25972 dvfsumleOLD 25973 dvfsumlem4 25982 dvfsumrlim3 25986 dvfsum2 25987 ftc1a 25990 ftc1lem4 25992 deg1add 26057 ply1divex 26090 ply1rem 26118 fta1glem2 26121 fta1blem 26123 ig1pdvds 26132 plyeq0lem 26162 dgrcolem2 26227 plydivlem4 26249 plyrem 26258 fta1lem 26260 aalioulem3 26287 aaliou2b 26294 aaliou3lem3 26297 aaliou3lem8 26298 ulmcn 26353 ulmdvlem1 26354 itgulm 26362 pserulm 26376 pserdvlem2 26383 abelthlem2 26387 abelthlem5 26390 abelthlem6 26391 abelthlem7 26393 abelthlem8 26394 abelthlem9 26395 sinq12gt0 26460 sinq34lt0t 26462 cosq14gt0 26463 cosq14ge0 26464 cos02pilt1 26478 efif1olem3 26496 argimgt0 26564 argimlt0 26565 logneg2 26567 logcnlem3 26596 logcnlem4 26597 logtayllem 26611 logtayl2 26614 cxpsqrtlem 26654 cxpsqrt 26655 cxpaddlelem 26704 abscxpbnd 26706 loglesqrt 26711 ang180lem2 26760 atanlogaddlem 26863 atanlogsublem 26865 atantan 26873 atans2 26881 atantayl 26887 leibpi 26892 log2tlbnd 26895 birthdaylem2 26902 birthdaylem3 26903 cxp2limlem 26926 jensenlem2 26938 jensen 26939 logdiflbnd 26945 emcllem2 26947 emcllem4 26949 harmonicbnd4 26961 fsumharmonic 26962 lgamgulmlem2 26980 lgamgulm2 26986 lgambdd 26987 lgamucov 26988 lgamcvglem 26990 lgamcvg2 27005 gamcvg 27006 wilthlem3 27020 basellem1 27031 basellem3 27033 basellem4 27034 fsumdvdsdiaglem 27133 dvdsppwf1o 27136 mpodvdsmulf1o 27144 dvdsmulf1o 27146 chteq0 27160 chtub 27163 chpub 27171 logfacubnd 27172 logfaclbnd 27173 logexprlim 27176 perfectlem2 27181 dchrfi 27206 bclbnd 27231 bposlem1 27235 bposlem3 27237 bposlem4 27238 bposlem6 27240 lgslem1 27248 lgsqrlem2 27298 lgsqrlem4 27300 lgseisenlem2 27327 lgsquadlem1 27331 lgsquadlem2 27332 lgsquad2lem1 27335 2sqlem3 27371 2sqlem4 27372 2sqlem8 27377 2sqlem11 27380 2sqcoprm 27386 2sqmod 27387 chebbnd1lem2 27421 chebbnd1lem3 27422 chtppilimlem1 27424 chpchtlim 27430 vmadivsum 27433 vmadivsumb 27434 rpvmasumlem 27438 dchrisumlem2 27441 dchrmusum2 27445 dchrvmasumlem2 27449 dchrvmasumlem3 27450 dchrisum0flblem2 27460 dchrisum0fno1 27462 dchrisum0re 27464 dchrisum0lem1 27467 dchrisum0lem2a 27468 mudivsum 27481 mulogsumlem 27482 mulog2sumlem2 27486 vmalogdivsum2 27489 selberglem2 27497 selbergb 27500 selberg2b 27503 logdivbnd 27507 selberg3lem1 27508 selberg3lem2 27509 selberg4lem1 27511 pntrmax 27515 pntrlog2bndlem2 27529 pntrlog2bndlem3 27530 pntrlog2bndlem5 27532 pntrlog2bndlem6a 27533 pntrlog2bndlem6 27534 pntrlog2bnd 27535 pntpbnd1a 27536 pntpbnd1 27537 pntpbnd2 27538 pntibndlem1 27540 pntibndlem2 27542 pntlemb 27548 pntlemq 27552 pntlemr 27553 pntlemj 27554 pntlemk 27557 qabvle 27576 padicabvcxp 27583 ostth2lem2 27585 ostth2lem3 27586 ostth2lem4 27587 ostth3 27589 addsuniflem 27936 negsid 27971 negsunif 27985 mulsuniflem 28067 sltmul2 28089 precsexlem9 28131 absmuls 28156 legtrid 28413 legov3 28420 krippenlem 28512 mideulem2 28556 midex 28559 opphllem5 28573 opphllem6 28574 opphl 28576 lmieu 28606 lmiisolem 28618 ttgcontlem1 28713 colinearalglem4 28738 axpaschlem 28769 axcontlem7 28799 nbfusgrlevtxm2 29209 clwlksndivn 29914 eucrct2eupth 30073 nvge0 30501 smcnlem 30525 nmoub3i 30601 nmoub2i 30602 nmlno0lem 30621 minvecolem2 30703 htthlem 30745 norm3dif2 30979 bcs2 31010 chscllem2 31466 eigposi 31664 nmopub2tALT 31737 nmfnleub2 31754 nmlnop0iALT 31823 riesz1 31893 cnlnadjlem2 31896 nmopcoadji 31929 leopsq 31957 leopmul 31962 leopnmid 31966 nmopleid 31967 opsqrlem6 31973 0leopj 32014 hstle1 32054 strlem3a 32080 mdslmd4i 32161 cvexchlem 32196 cdj1i 32261 unidifsnel 32349 unidifsnne 32350 le2halvesd 32543 xlt2addrd 32546 fsumub 32609 wrdt2ind 32692 xrge0tsmsd 32789 fzto1st1 32841 cycpmco2lem4 32868 cycpmco2lem6 32870 cyc3conja 32896 archiabllem1a 32917 archiabllem2a 32920 archiabllem2c 32921 orngsqr 33037 ornglmulle 33038 orngrmulle 33039 orng0le1 33045 fedgmullem1 33332 fedgmullem2 33333 algextdeglem8 33397 metideq 33499 metider 33500 sqsscirc1 33514 esummono 33678 esumpad2 33680 esumle 33682 esumlef 33686 esumcst 33687 esumrnmpt2 33692 esum2d 33717 aean 33868 dya2ub 33895 dya2icoseg 33902 omssubadd 33925 inelcarsg 33936 carsgsigalem 33940 carsggect 33943 carsgclctunlem2 33944 eulerpartlemb 33993 fibp1 34026 sgnmulsgp 34175 signsplypnf 34187 signsply0 34188 fdvposlt 34236 fdvposle 34238 reprgt 34258 logdivsqrle 34287 hgt750lemb 34293 hgt750leme 34295 tgoldbachgtde 34297 subfacval3 34804 sconnpht2 34853 sconnpi1 34854 resconn 34861 snmlff 34944 sinccvglem 35281 faclimlem2 35343 btwnouttr2 35623 dnibndlem5 35962 dnibndlem7 35964 dnibndlem8 35965 dnibndlem9 35966 dnibndlem10 35967 dnibnd 35971 knoppcnlem4 35976 knoppcnlem9 35981 unbdqndv2lem1 35989 unbdqndv2lem2 35990 knoppndvlem11 36002 knoppndvlem12 36003 knoppndvlem14 36005 knoppndvlem15 36006 knoppndvlem17 36008 knoppndvlem18 36009 knoppndvlem19 36010 knoppndvlem21 36012 ltflcei 37086 poimirlem9 37107 poimirlem26 37124 poimirlem27 37125 poimirlem29 37127 heicant 37133 mblfinlem2 37136 mblfinlem3 37137 mblfinlem4 37138 volsupnfl 37143 itg2addnclem 37149 itg2addnclem3 37151 iblmulc2nc 37163 ftc1cnnclem 37169 ftc1anclem6 37176 ftc1anclem7 37177 ftc1anclem8 37178 ftc2nc 37180 dvasin 37182 geomcau 37237 bfplem2 37301 rrncmslem 37310 rrnequiv 37313 lsatcvatlem 38525 islshpcv 38529 atlatmstc 38795 cvlsupr7 38824 cvrval3 38890 cvrval5 38892 cvrexchlem 38896 atcvrj1 38908 cvrat3 38919 cvrat4 38920 atbtwn 38923 1cvratex 38950 hlatexch4 38958 3atlem1 38960 3atlem2 38961 atcvrlln2 38996 atcvrlln 38997 lplnllnneN 39033 llncvrlpln2 39034 4atlem3b 39075 lplncvrlvol2 39092 dalemswapyz 39133 dalemswapyzps 39167 dalem25 39175 dalem39 39188 dalem58 39207 dalem59 39208 lneq2at 39255 lncvrat 39259 dalawlem2 39349 dalawlem3 39350 dalawlem4 39351 dalawlem6 39353 dalawlem9 39356 dalawlem11 39358 dalawlem12 39359 lhpocnle 39493 lhpmcvr3 39502 lhpmcvr5N 39504 lhpmcvr6N 39505 4atexlemunv 39543 4atexlemc 39546 4atexlemex2 39548 lautm 39571 cdlemc2 39669 cdleme5 39717 cdleme11j 39744 cdleme16b 39756 cdlemednpq 39776 cdleme19e 39784 cdleme20i 39794 cdleme22a 39817 cdleme22cN 39819 cdleme22d 39820 cdleme22e 39821 cdleme22eALTN 39822 cdleme22f 39823 cdleme23c 39828 cdleme30a 39855 cdleme35a 39925 cdleme35b 39927 cdleme42h 39959 cdlemeg46rgv 40005 cdlemg8b 40105 cdlemg12e 40124 cdlemg13a 40128 cdlemg17pq 40149 cdlemg18c 40157 cdlemg19 40161 cdlemg21 40163 cdlemg31d 40177 cdlemg33a 40183 tendoid 40250 cdlemk4 40311 cdlemki 40318 cdlemk10 40320 cdlemksv2 40324 cdlemk12 40327 cdlemk14 40331 cdlemk15 40332 cdlemk1u 40336 cdlemk5u 40338 cdlemk12u 40349 cdlemk45 40424 cdlemk48 40427 dia2dimlem1 40541 dia2dimlem2 40542 dia2dimlem3 40543 cdlemm10N 40595 cdlemn2 40672 dihjustlem 40693 dihglbcpreN 40777 dihmeetlem3N 40782 nnproddivdvdsd 41475 lcmineqlem17 41520 lcmineqlem18 41521 3lexlogpow2ineq1 41533 3lexlogpow2ineq2 41534 3lexlogpow5ineq5 41535 aks4d1p1p3 41544 aks4d1p1p2 41545 aks4d1p1p4 41546 aks4d1p1p5 41550 aks4d1p1 41551 aks4d1p3 41553 aks4d1p8 41562 posbezout 41575 primrootspoweq0 41581 aks6d1c1 41591 hashscontpow1 41596 aks6d1c4 41599 aks6d1c2 41605 aks6d1c5lem1 41611 aks6d1c5lem3 41612 aks6d1c5lem2 41613 deg1gprod 41616 sticksstones7 41628 sticksstones10 41631 sticksstones12 41634 sticksstones22 41644 aks6d1c6lem1 41646 aks6d1c6lem3 41648 aks6d1c6lem4 41649 bcled 41654 bcle2d 41655 aks6d1c7lem1 41656 2xp3dxp2ge1d 41697 factwoffsmonot 41698 evlselv 41823 zrtdvds 41908 rtprmirr 41909 dffltz 42061 fltdvdsabdvdsc 42065 fltaccoprm 42067 fltabcoprm 42069 flt4lem5elem 42078 flt4lem7 42086 fltnlta 42090 irrapxlem1 42245 pell1qrgaplem 42296 pell1qrgap 42297 monotoddzzfi 42366 jm2.24nn 42383 congtr 42389 congmul 42391 congsub 42394 fzmaxdif 42405 acongeq 42407 jm2.20nn 42421 jm2.25 42423 hbtlem4 42553 dgrsub2 42562 mpaaeu 42577 idomsubgmo 42624 iscard4 42966 sqrtcvallem4 43072 leeq2d 43591 int-sqgeq0d 43619 int-ineqmvtd 43624 cvgdvgrat 43753 radcnvrat 43754 hashnzfzclim 43762 dvconstbi 43774 binomcxplemdvbinom 43793 isosctrlem1ALT 44376 mulltgt0 44387 rnmptbd2lem 44626 oddfl 44661 2timesgt 44672 lt3addmuld 44685 lt4addmuld 44690 supxrgere 44717 supxrgelem 44721 supxrge 44722 xadd0ge2 44725 infrpge 44735 xrlexaddrp 44736 xralrple2 44738 infxr 44751 infleinflem1 44754 infleinflem2 44755 infleinf 44756 xralrple4 44757 xralrple3 44758 recnnltrp 44761 rpgtrecnn 44764 xrralrecnnge 44774 rexabslelem 44802 infrnmptle 44807 supminfxr 44848 xrpnf 44870 iccshift 44905 iooshift 44909 ressiocsup 44941 ressioosup 44942 fsumnncl 44962 fmul01 44970 fmul01lt1lem1 44974 fmul01lt1lem2 44975 mccllem 44987 climrec 44993 climexp 44995 climneg 45000 limcrecl 45019 sumnnodd 45020 lptioo2 45021 lptioo1 45022 ltmod 45028 lptre2pt 45030 0ellimcdiv 45039 limclner 45041 fnlimcnv 45057 climinf2lem 45096 limsupubuzlem 45102 limsup10exlem 45162 limsupgtlem 45167 dfxlim2v 45237 xlimliminflimsup 45252 cncficcgt0 45278 cncfioobdlem 45286 ioodvbdlimc1lem1 45321 ioodvbdlimc1lem2 45322 ioodvbdlimc2lem 45324 dvdsn1add 45329 dvnxpaek 45332 dvnmul 45333 dvnprodlem1 45336 itgiccshift 45370 itgperiod 45371 sublevolico 45374 ismbl3 45376 ovolsplit 45378 ismbl4 45383 stoweidlem1 45391 stoweidlem11 45401 stoweidlem13 45403 stoweidlem26 45416 stoweidlem34 45424 stoweidlem38 45428 stoweidlem42 45432 stoweidlem51 45441 stoweidlem59 45449 stirlinglem5 45468 stirlinglem6 45469 stirlinglem7 45470 stirlinglem10 45473 stirlinglem11 45474 stirlinglem13 45476 stirlinglem15 45478 dirkercncflem1 45493 dirkercncflem4 45496 fourierdlem4 45501 fourierdlem10 45507 fourierdlem11 45508 fourierdlem15 45512 fourierdlem20 45517 fourierdlem25 45522 fourierdlem26 45523 fourierdlem30 45527 fourierdlem37 45534 fourierdlem39 45536 fourierdlem40 45537 fourierdlem41 45538 fourierdlem42 45539 fourierdlem44 45541 fourierdlem47 45543 fourierdlem48 45544 fourierdlem49 45545 fourierdlem50 45546 fourierdlem51 45547 fourierdlem52 45548 fourierdlem54 45550 fourierdlem60 45556 fourierdlem61 45557 fourierdlem63 45559 fourierdlem64 45560 fourierdlem65 45561 fourierdlem73 45569 fourierdlem74 45570 fourierdlem75 45571 fourierdlem76 45572 fourierdlem78 45574 fourierdlem79 45575 fourierdlem81 45577 fourierdlem84 45580 fourierdlem87 45583 fourierdlem92 45588 fourierdlem93 45589 fourierdlem101 45597 fourierdlem102 45598 fourierdlem103 45599 fourierdlem104 45600 fourierdlem111 45607 fourierdlem114 45610 sqwvfoura 45618 sqwvfourb 45619 fouriersw 45621 etransclem19 45643 etransclem23 45647 etransclem24 45648 etransclem25 45649 etransclem27 45651 etransclem32 45656 etransclem35 45659 etransclem48 45672 qndenserrnbllem 45684 ioorrnopnlem 45694 ioorrnopnxrlem 45696 fsumlesge0 45767 sge0cl 45771 sge0supre 45779 sge0less 45782 sge0gerp 45785 sge0ltfirp 45790 sge0le 45797 sge0ltfirpmpt 45798 sge0split 45799 sge0rpcpnf 45811 sge0ltfirpmpt2 45816 sge0isum 45817 sge0xaddlem1 45823 sge0pnffigtmpt 45830 sge0pnffsumgt 45832 sge0gtfsumgt 45833 sge0seq 45836 nnfoctbdjlem 45845 meassle 45853 meaiuninclem 45870 meaiininclem 45876 omeiunle 45907 omeiunltfirp 45909 carageniuncllem2 45912 carageniuncl 45913 omess0 45924 hoicvr 45938 ovnlerp 45952 ovnsubaddlem1 45960 hsphoidmvle2 45975 hoidmv1lelem2 45982 hoidmv1le 45984 hoidmvlelem1 45985 hoidmvlelem2 45986 hoidmvlelem3 45987 hoidmvlelem5 45989 ovnhoilem2 45992 ovnhoi 45993 hoidifhspdmvle 46010 hoiqssbllem2 46013 hspmbllem2 46017 hspmbllem3 46018 hspmbl 46019 vonioolem2 46071 vonicclem2 46074 smfaddlem1 46153 smflimlem2 46162 smflimlem4 46164 smfmullem1 46181 smfinflem 46207 smflimsuplem4 46213 smflimsuplem8 46217 perfectALTVlem2 47064 nnpw2blen 47704 itscnhlinecirc02plem1 47906

Copyright terms: Public domain

	
		OSZAR »