Theorem bitrdi 287

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
bitrdi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrdi.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
bitrdi	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bitr2di  288  bitr4di  289  3bitr3g  313  bibi2i  337  ibibr  368  biancomd  463  pm5.75  1031  19.17  2234  sb2ae  2501  sbcom3  2511  sbal1  2533  sbal2  2534  eqabrd  2878  cbvralf  3332  cbvreu  3393  cbvrabwOLD  3437  cbvrab  3441  ceqsralt  3477  ralxpxfr2d  3602  clel2g  3615  clel4g  3619  elabd2  3626  ralab2  3657  rexab2  3659  reu7  3692  reu8  3693  2reu5  3718  ru  3740  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  ralss  4010  ralssOLD  4012  rexssOLD  4013  sbcssg  4476  rabsneq  4601  elpwunsn  4643  reuprg0  4661  reuprg  4662  prssg  4777  ssunsn2  4785  eqsn  4787  prneimg2  4813  preqsnd  4817  2ralunsn  4853  eluniab  4879  csbuni  4895  elintabg  4915  dfiin2g  4988  disjprg  5096  disjxun  5098  cbvopab1g  5175  cbvmptf  5200  cbvmptfg  5201  al0ssb  5255  reusv3  5352  elopg  5422  opthneg  5437  opeqsng  5459  sotrieq2  5572  frsn  5720  eliunxp  5794  exopxfr2  5801  relop  5807  eldm2g  5856  reldm0  5885  relrn0  5930  restidsing  6020  elimasng  6056  asymref2  6082  somin1  6098  imadifssran  6117  xpnz  6125  xpcan  6142  xpcan2  6143  relsn2  6178  dfpo2  6262  ordtri2  6360  ordtri3  6361  oneqmini  6378  cbviota  6465  iotaval2  6471  iota1  6479  sniota  6491  fncnv  6573  fnres  6627  sbcfng  6667  sbcfg  6668  brprcneu  6832  brprcneuALT  6833  fnopfvb  6893  fvelrnb  6902  funimass4  6906  unima  6917  dffv2  6937  fvopab3g  6944  eqfnfv  6985  eqfnfv3  6987  eqfnfv2f  6989  fvreseq0  6992  fnreseql  7002  fniniseg  7014  respreima  7020  rexrn  7041  ralrn  7042  f1ompt  7065  fssrescdmd  7081  fsn  7090  funopsn  7103  funsndifnop  7106  fprb  7150  tpres  7157  eufnfv  7185  ralima  7193  reximaOLD  7195  ralimaOLD  7196  dff13  7210  f13dfv  7230  fliftfun  7268  isocnv  7286  isoini  7294  f1oiso  7307  fnssintima  7318  imaeqsexvOLD  7319  cbvriota  7338  riotaeqimp  7351  eusvobj2  7360  oprabidw  7399  oprabid  7400  f1opr  7424  eloprabga  7477  resoprab  7486  eqfnov  7497  eqfnov2  7498  ov6g  7532  ovelrn  7544  funimassov  7545  ovelimab  7546  ndmovg  7551  caovord2  7580  imaeqexov  7606  imaeqalov  7607  tfisi  7811  eqop  7985  releldm2  7997  dfoprab4  8009  opiota  8013  bropopvvv  8042  bropfvvvv  8044  fparlem1  8064  fparlem2  8065  xporderlem  8079  poxp  8080  soxp  8081  fnwelem  8083  xpord2lem  8094  poxp2  8095  frxp2  8096  xpord2indlem  8099  poxp3  8102  frxp3  8103  xpord3pred  8104  xpord3inddlem  8106  elsuppfng  8121  elsuppfn  8122  rexsupp  8134  suppcoss  8159  mpoxopovel  8172  brtpos2  8184  brtpos0  8185  rntpos  8191  dftpos3  8196  tpostpos  8198  tpossym  8210  tposoprab  8214  mpocurryd  8221  frrlem1  8238  oevn0  8452  om00el  8513  omordlim  8514  omlimcl  8515  oeoa  8535  oeoe  8537  oeeulem  8539  oeeui  8540  oaabs2  8587  omabs  8589  cofonr  8612  naddunif  8631  naddasslem1  8632  naddasslem2  8633  erth2  8701  qliftfun  8751  erovlem  8762  ecopovsym  8768  mapdm0  8791  elpmg  8792  elpm2g  8793  dom2lem  8941  mapsnend  8985  xpdom2  9012  omxpenlem  9018  0sdomg  9046  fodomr  9068  xpf1o  9079  mapen  9081  ac6sfi  9196  fodomfir  9240  mapfien  9323  marypha2lem3  9352  ordtypelem7  9441  wemaplem1  9463  wemapsolem  9467  elharval  9478  brwdom3  9499  unwdomg  9501  xpwdomg  9502  inf3lem1  9549  cantnfs  9587  cantnfp1lem2  9600  cantnflem1d  9609  cantnflem1  9610  wemapwe  9618  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  r1sdom  9698  rankr1ai  9722  rankval2  9742  unbndrank  9766  rankunb  9774  tcrank  9808  bnd2  9817  cardnueq0  9888  iscard2  9900  r0weon  9934  fseqenlem1  9946  alephord2  9998  cardaleph  10011  aceq0  10040  dfac5lem4OLD  10050  dfac5  10051  kmlem14  10086  cfsmolem  10192  isfin4-2  10236  fin23lem26  10247  fin23lem22  10249  fin1a2lem7  10328  axdc3lem2  10373  axdc3  10376  zfac  10382  zornn0g  10427  axdclem  10441  brdom3  10450  zfcndac  10542  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  pwfseqlem3  10583  winainflem  10616  eltsk2g  10674  inatsk  10701  axgroth2  10748  axgroth6  10751  sstskm  10765  ltexpi  10825  ordpinq  10866  lterpq  10893  ltanq  10894  ltmnq  10895  genpv  10922  genpelv  10923  prlem934  10956  prlem936  10970  addcmpblnr  10992  ltsrpr  11000  ltsosr  11017  mulgt0sr  11028  supsrlem  11034  elreal2  11055  ltresr  11063  ltresr2  11064  axrrecex  11086  axpre-ltadd  11090  axpre-mulgt0  11091  axpre-sup  11092  subcan2  11418  negcon1  11445  negcon2  11446  lt0neg1  11655  lt0neg2  11656  le0neg1  11657  le0neg2  11658  msq0d  11799  mulcan2g  11803  divmul2  11812  reclt1  12049  recgt1  12050  infm3  12113  suprlub  12118  suprleub  12120  infregelb  12138  addltmul  12389  arch  12410  elznn0  12515  nn0lt2  12567  eluz1  12767  raluz  12821  rexuz  12823  nnwof  12839  cnref1o  12910  ltxr  13041  xrltlen  13072  dflt2  13074  xrrebnd  13095  xlt0neg1  13146  xlt0neg2  13147  xle0neg1  13148  xle0neg2  13149  xmulneg1  13196  supxrbnd  13255  elixx1  13282  ixxun  13289  elioo2  13314  elicc4  13341  elioopnf  13371  elioomnf  13372  iccneg  13400  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  iccf1o  13424  elfz1  13440  0fz1  13472  elfzp1  13502  fzpr  13507  uzsplit  13524  elfzm1b  13530  elfzp12  13531  fznn0  13547  fvinim0ffz  13717  injresinj  13719  fleqceilz  13786  zmodid2  13831  fsuppmapnn0fiub0  13928  bernneq  14164  hasheqf1o  14284  euhash1  14355  hashbclem  14387  hashfacen  14389  hashf1  14392  hashge2el2difr  14416  hashtpg  14420  ccatrn  14525  pfxsuffeqwrdeq  14633  wrd2ind  14658  scshwfzeqfzo  14761  wwlktovf1  14892  brtrclfv  14937  2shfti  15015  sqrtmsq2i  15323  limsupgle  15412  limsuple  15413  rlim  15430  clim0  15441  ello12  15451  elo12  15462  o1lo1  15472  rlimresb  15500  lo1add  15562  lo1mul  15563  rlimno1  15589  summo  15652  fsumsplit  15676  mertenslem2  15820  prodmo  15871  fprodsplit  15901  fprod2dlem  15915  cnso  16184  sqrt2irr  16186  dvdsval2  16194  alzdvds  16259  odd2np1lem  16279  even2n  16281  sumodd  16327  divalgb  16343  divalgmod  16345  bitsval  16363  bitsmod  16375  sadcp1  16394  gcddvds  16442  bezoutlem3  16480  bezout  16482  lcmfunsnlem2  16579  isprm3  16622  prmind2  16624  dvdsprime  16626  ge2nprmge4  16640  coprm  16650  prmdvdsexp  16654  crth  16717  pythagtriplem2  16757  pythagtrip  16774  pceu  16786  pc11  16820  vdwapval  16913  vdwapun  16914  vdwlem10  16930  vdwlem12  16932  vdwlem13  16933  ramval  16948  ramub1lem2  16967  prmlem0  17045  elrest  17359  imasleval  17474  ismri  17566  isacs  17586  isacs2  17588  acsfn1  17596  iscatd2  17616  homfeq  17629  catpropd  17644  ismon  17669  issect  17689  issect2  17690  isinv  17696  cic  17735  isssc  17756  isfunc  17800  funcres2b  17833  isnat  17886  fucinv  17912  iszeroo  17934  elhoma  17968  setcinv  18026  isprs  18231  isdrs  18236  lubeldm  18286  glbeldm  18299  istos  18351  tosso  18352  latnle  18408  latdisd  18432  isdlat  18457  isipodrs  18472  isacs5  18483  chnccat  18561  ismgmhm  18633  issubmgm  18639  ismhm  18722  issubm  18740  issubmndb  18742  sursubmefmnd  18833  injsubmefmnd  18834  grpsubeq0  18968  grpsubadd  18970  issubg  19068  subgmulg  19082  issubg3  19086  isnsg  19096  eqger  19119  eqglact  19120  eqgid  19121  cycsubmel  19141  isghm  19156  isghmOLD  19157  isga  19232  gacan  19246  gaorb  19248  gastacos  19251  orbsta  19254  elcntz  19263  elcntzsn  19266  sscntz  19267  gsmsymgreq  19373  psgnunilem5  19435  psgnunilem3  19437  psgneldm2  19445  psgneu  19447  psgnfitr  19458  dfod2  19505  isslw  19549  sylow2alem2  19559  lsmelvalx  19581  lsmcom2  19596  lsmass  19610  lssnle  19615  pj1eu  19637  lsmhash  19646  efgi  19660  efgval2  19665  efgtlen  19667  efgred  19689  lsmcomx  19797  iscyggen2  19822  iscyg3  19827  gsumval3eu  19845  gsumzsplit  19868  eldprd  19947  subgdmdprd  19977  dprddisj2  19982  dprd2da  19985  dmdprdsplit2lem  19988  dmdprdsplit2  19989  dprdsplit  19991  dmdprdpr  19992  pgpfac1lem3  20020  pgpfac1lem4  20021  pgpfac1lem5  20022  srgfcl  20143  dvdsr02  20320  isunit  20321  isirred  20367  isrnghmmul  20390  isrngim  20393  c0snmgmhm  20410  isrhm  20426  isrim0  20430  isnzr2  20463  0ringnnzr  20470  subsubrng2  20509  subsubrg2  20544  issubrg3  20545  rngcinv  20582  ringcinv  20616  isdomn3  20660  drngunit  20679  issdrg  20733  isabv  20756  islmod  20827  islss  20897  ellspsn  20966  islmhm  20991  lmhmeql  21019  islbs  21040  lsmspsn  21048  lsmelval2  21049  lspprel  21058  lvecvscan2  21079  lvecinv  21080  lspsneq  21089  lspsneu  21090  lspsolvlem  21109  islpidl  21292  lidldvgen  21301  prmirredlem  21439  zrhrhmb  21477  zndvds  21516  elocv  21635  iscss  21650  pjdm  21674  ishil2  21686  isobs  21687  obslbs  21697  frlmelbas  21723  ellspd  21769  islinds  21776  islindf4  21805  aspval2  21866  mplsubglem  21966  mpllsslem  21967  mplmonmul  22003  opsrtoslem2  22023  ismhp  22095  mat1dimelbas  22427  dmatel  22449  scmatel  22461  mdetunilem8  22575  mdetunilem9  22576  maducoeval2  22596  cramer0  22646  cpmatel  22667  istop2g  22852  istopon  22868  toprntopon  22881  isbasis2g  22904  isbasis3g  22905  tgss2  22943  bastop1  22949  iscld  22983  elcls  23029  ntreq0  23033  isclo  23043  isclo2  23044  islp  23096  lpdifsn  23099  islpi  23105  restsn  23126  restlp  23139  ordtbaslem  23144  ordtbas2  23147  lmbr  23214  cnprest2  23246  ist0-3  23301  ist1-2  23303  cmpsublem  23355  cmpfi  23364  1stcrest  23409  2ndcdisj  23412  1stccnp  23418  llyi  23430  nllyi  23431  lly1stc  23452  iskgen3  23505  kgencn  23512  txbas  23523  eltx  23524  elpt  23528  xkoccn  23575  ptcnplem  23577  hausdiag  23601  hauseqlcld  23602  txlm  23604  txkgen  23608  kqfvima  23686  kqt0lem  23692  r0cld  23694  regr1lem2  23696  hmeoimaf1o  23726  isfbas2  23791  fbssfi  23793  trfbas2  23799  trfil2  23843  fmfnfmlem4  23913  elflim2  23920  flimrest  23939  cnflf  23958  txflf  23962  fclsopn  23970  ufilcmp  23988  cnfcf  23998  alexsubALTlem4  24006  cnextf  24022  tmdcn2  24045  qustgpopn  24076  qustgplem  24077  eltsms  24089  tsmsgsum  24095  tsmssplit  24108  elutop  24189  ustuqtop  24202  utopsnneiplem  24203  isusp  24217  isucn  24233  iscfilu  24243  ispsmet  24260  ismet  24279  isxmet  24280  metn0  24316  elblps  24343  elbl  24344  metrest  24480  metuel2  24521  psmetutop  24523  restmetu  24526  dscmet  24528  nrmmetd  24530  isngp3  24554  nmogelb  24672  isnmhm  24702  qtopbaslem  24714  xrsxmet  24766  icccmplem2  24780  metdseq0  24811  elcncf  24850  cnheibor  24922  ishtpy  24939  isphtpy  24948  isphtpc  24961  om1elbas  25000  elpi1  25013  isclmp  25065  nmhmcn  25088  iscph  25138  tcphcph  25205  lmmbrf  25230  iscfil  25233  iscfil2  25234  iscau  25244  caucfil  25251  iscmet  25252  iscmet3  25261  cfilucfil3  25288  bcthlem1  25292  rrxcph  25360  minveclem3b  25396  minveclem6  25402  evthicc2  25429  ovolfioo  25436  ovolficc  25437  ovolshftlem1  25478  ovolscalem1  25482  iundisj2  25518  dyadmbl  25569  volsup2  25574  mbfmax  25618  mbfsup  25633  mbfinf  25634  i1f1lem  25658  i1fres  25674  itg1climres  25683  itg2leub  25703  itg2seq  25711  itg2splitlem  25717  itg2monolem1  25719  itg2mono  25722  itg2cn  25732  iblpos  25762  iblcn  25768  itgsplit  25805  ellimc2  25846  dvreslem  25878  elcpn  25904  rolle  25962  dvlip  25966  dvivth  25983  tdeglem4  26033  mdegleb  26037  deg1ldg  26065  ply1nzb  26096  ply1divmo  26109  ply1divex  26110  fta1glem2  26142  plyco0  26165  elply  26168  coeeu  26198  plydivex  26273  taylthlem2  26350  taylthlem2OLD  26351  radcnvlt1  26395  sincosq1sgn  26475  sincosq2sgn  26476  coseq1  26502  logreclem  26740  affineequiv  26801  affineequiv4  26804  dcubic  26824  quart  26839  atans2  26909  efrlim  26947  efrlimOLD  26948  mumullem2  27158  dvdsflsumcom  27166  fsumvma2  27193  chpchtsum  27198  chpub  27199  dchrelbas  27215  dchrelbas2  27216  dchreq  27237  dchrptlem2  27244  gausslemma2dlem0i  27343  lgsquadlem2  27360  m1lgs  27367  2lgsoddprmlem3  27393  2sqlem6  27402  2sqlem9  27406  2sqlem10  27407  2sq2  27412  2sqreunnltb  27440  2sqreuop  27441  2sqreuopnn  27442  2sqreuoplt  27443  2sqreuopltb  27444  2sqreuopnnlt  27445  2sqreuopnnltb  27446  2sqreuopb  27447  dchrisum0flb  27489  pntpbnd1  27565  pntlem3  27588  pntlemp  27589  ltsval2  27636  ltsintdifex  27641  ltsres  27642  noextenddif  27648  nosepssdm  27666  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupno  27683  nosupbnd1lem1  27688  noinfcbv  27697  noinfno  27698  noinfdm  27699  noinfres  27702  noinfbnd1lem1  27703  lestri3  27735  cutbdaylt  27806  ltsrec  27809  elold  27867  sltsleft  27868  sltsright  27869  madebdayim  27896  madebdaylemlrcut  27907  madebday  27908  newbday  27910  ltslpss  27916  cofcutr  27932  cofcutrtime  27935  addsval2  27971  addsrid  27972  addsprop  27984  negsprop  28043  lt0negs2d  28059  subadds  28078  mulsval2lem  28118  mulsrid  28121  mulsprop  28138  mulscom  28147  mulsunif2  28178  mulscan2d  28187  precsexlemcbv  28214  precsexlem9  28223  recsex  28227  absnegs  28255  onsfi  28364  n0lts1e0  28376  bdayn0p1  28377  bdayn0sf1o  28378  dfnns2  28380  eucliddivs  28384  elnnzs  28409  elznns  28410  n0seo  28429  pw2recs  28446  avglts1d  28461  avglts2d  28462  bdaypw2n0bndlem  28471  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  z12bdaylem1  28478  z12zsodd  28490  z12bday  28493  bdayfin  28495  recut  28502  renegscl  28506  remulscl  28510  istrkg2ld  28544  iscgrg  28596  tgcgr4  28615  isismt  28618  tgellng  28637  tgcolg  28638  legov  28669  lnhl  28699  lmimid  28878  iscgra1  28894  ttgelitv  28967  elee  28978  mpteleeOLD  28980  colinearalglem2  28992  colinearalg  28995  ax5seglem5  29018  axeuclidlem  29047  axeuclid  29048  axcontlem1  29049  axcontlem2  29050  axcontlem5  29053  axcontlem7  29055  wrdupgr  29170  wrdumgr  29182  uhgrspansubgrlem  29375  nbgrel  29425  nbupgrel  29430  nbgr2vtx1edg  29435  nbuhgr2vtx1edgblem  29436  nbuhgr2vtx1edgb  29437  nb3grprlem2  29466  nb3grpr2  29468  uvtx01vtx  29482  uvtxusgrel  29488  iscplgr  29500  vtxdun  29567  fusgrn0degnn0  29585  1loopgrnb0  29588  umgr2v2enb1  29612  vdiscusgrb  29616  wlkl1loop  29723  wlkv0  29735  wlklenvclwlk  29739  upgr2wlk  29752  wlkp1lem8  29764  upgrtrls  29785  upgristrl  29786  dfpth2  29814  isspthonpth  29834  usgr2trlncl  29845  usgr2pthlem  29848  usgr2pth  29849  pthdlem1  29851  isclwlke  29862  isclwlkupgr  29863  uspgrn2crct  29893  wwlks  29920  iswwlksn  29923  wwlksnext  29978  wwlksnextinj  29984  wspn0  30009  wpthswwlks2on  30049  rusgrnumwwlkl1  30056  rusgrnumwwlkslem  30057  rusgrnumwwlkb0  30059  clwlkclwwlk  30089  clwwlknwwlksn  30125  clwwlkn2  30131  clwwlkel  30133  clwwlkwwlksb  30141  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknon1loop  30185  0wlk  30203  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  dfconngr1  30275  vdn0conngrumgrv2  30283  eupth2lem2  30306  eupth2lem3lem6  30320  eucrct2eupth  30332  isfrgr  30347  frgr3v  30362  frgrncvvdeqlem3  30388  frgrncvvdeqlem6  30391  frgrwopreglem2  30400  fusgreg2wsplem  30420  2clwwlkel  30436  extwwlkfabel  30440  numclwwlk1lem2f1  30444  numclwwlk1lem2fo  30445  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  nrt2irr  30560  isgrpo  30584  isssp  30811  islno  30840  nmogtmnf  30857  nmoubi  30859  nmounbi  30863  isblo  30869  ishmo  30898  ubthlem1  30957  ubthlem2  30958  minvecolem5  30968  minvecolem6  30969  hvmulcan2  31160  hire  31181  ocel  31368  ocsh  31370  pjhthmo  31389  shscom  31406  shmodsi  31476  elspani  31630  adjsym  31920  eigorthi  31924  nmopgtmnf  31955  adjeu  31976  adjval2  31978  cnvadj  31979  nmopub  31995  nmfnleub  32012  eleigvec  32044  nmop0h  32078  largei  32354  mdbr2  32383  mddmd2  32396  mdsl2i  32409  chrelat3  32458  atnemeq0  32464  chirredlem1  32477  sumdmdii  32502  sumdmdlem  32505  dmdbr5ati  32509  cdjreui  32519  nelun  32599  tpssg  32623  disjabrex  32668  disjabrexf  32669  iundisj2f  32676  disjunsn  32680  brab2d  32694  br8d  32697  opabdm  32700  opabrn  32701  nfpconfp  32721  ofpreima  32754  funcnv5mpt  32756  suppiniseg  32775  1stpreima  32796  curry2ima  32798  f1od2  32808  fpwrelmap  32822  infxrge0gelb  32856  xnn01gt  32860  nndiffz1  32876  iundisj2fi  32887  fzo0opth  32893  sgn3da  32925  ind1a  32948  tlt3  33062  toslublem  33064  tosglblem  33066  ismnt  33075  cntzun  33172  isfxp  33261  isarchi2  33278  erler  33358  domnprodeq0  33369  qusker  33441  unitprodclb  33481  lsmsnorb  33483  lsmssass  33494  grplsm0l  33495  isprmidl  33530  ismxidl  33554  mxidlirred  33564  isrprm  33609  ufdprmidl  33633  1arithufdlem4  33639  ply1degltel  33686  ply1degleel  33687  psrmonmul  33726  vieta  33756  elirng  33863  algextdeglem8  33901  fldext2chn  33905  constrextdg2  33926  constrfiss  33928  smatrcl  33973  zarcls  34051  rhmpreimacnlem  34061  cnvordtrestixx  34090  ordtconnlem1  34101  fsumcvg4  34127  lmdvg  34130  esum2dlem  34269  braew  34419  ismbfm  34428  mbfmcnt  34445  issibf  34510  eulerpartgbij  34549  eulerpartlemgvv  34553  eulerpartlemgh  34555  elorvc  34637  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemodife  34675  reprinrn  34795  reprdifc  34804  bnj1366  35004  bnj984  35127  bnj1171  35175  bnj1253  35192  bnj1417  35216  bnj1452  35227  rankval2b  35274  lfuhgr3  35333  subfacp1lem3  35395  subfacp1lem5  35397  subfacp1lem6  35398  erdszelem9  35412  erdszelem10  35413  erdsze2lem2  35417  iscvm  35472  cvmlift2lem10  35525  snmlval  35544  satfv1  35576  satfvsucsuc  35578  satfrnmapom  35583  satf0op  35590  satf0n0  35591  sat1el2xp  35592  fmlafvel  35598  fmlaomn0  35603  gonarlem  35607  fmla0disjsuc  35611  fmlasucdisj  35612  satffunlem1lem1  35615  satffunlem2lem1  35617  satefvfmla0  35631  sategoelfvb  35632  mclsppslem  35796  r1peuqusdeg1  35856  climuzcnv  35884  br6  35970  elintfv  35978  dfdm5  35986  dfrn5  35987  dfon2lem7  36000  dfon2  36003  dfrdg2  36006  elfuns  36126  dfiota3  36134  brimg  36148  dfrdg4  36164  btwnouttr  36237  btwnexch  36238  funtransport  36244  cgr3permute1  36261  colinearperm1  36275  brsegle  36321  outsideoftr  36342  outsideofeu  36344  funray  36353  funline  36355  lineunray  36360  lineelsb2  36361  nn0prpwlem  36535  nn0prpw  36536  fneval  36565  topfneec  36568  filnetlem4  36594  ordcmp  36660  regsfromregtr  36687  regsfromsetind  36688  bj-sblem  37083  bj-sbceqgALT  37141  bj-elgab  37178  bj-clel3gALT  37287  bj-restpw  37336  bj-elid6  37414  bj-eldiag  37420  bj-eldiag2  37421  bj-imdirco  37434  f1omptsnlem  37580  mptsnunlem  37582  topdifinfeq  37594  isbasisrelowllem1  37599  isbasisrelowllem2  37600  relowlpssretop  37608  fvineqsnf1  37654  fvineqsneu  37655  wl-ifpimpr  37710  wl-sbcom2d  37805  wl-sbalnae  37806  curf  37838  unccur  37843  phpreu  37844  finixpnum  37845  ptrest  37859  poimirlem8  37868  poimirlem17  37877  poimirlem18  37878  poimirlem20  37880  poimirlem21  37881  poimirlem23  37883  poimirlem26  37886  poimirlem27  37887  poimirlem28  37888  poimirlem31  37891  poimirlem32  37892  poimir  37893  heicant  37895  mblfinlem1  37897  ismblfin  37901  mbfresfi  37906  itg2addnclem  37911  itg2addnclem2  37912  itg2addnc  37914  itg2gt0cn  37915  ftc1anclem6  37938  unirep  37954  indexa  37973  sdclem1  37983  fdc  37985  neificl  37993  istotbnd  38009  sstotbnd2  38014  isbnd  38020  isbnd3b  38025  heibor1lem  38049  heiborlem3  38053  rrnheibor  38077  ismgmOLD  38090  rngosn3  38164  isrngohom  38205  isrngoiso  38218  iscrngo2  38237  isidl  38254  ispridl  38274  pridlidl  38275  pridlnr  38276  pridl  38277  ismaxidl  38280  maxidlidl  38281  smprngopr  38292  prnc  38307  eldmres  38517  eldmressnALTV  38519  eldmqsres  38533  ideq2  38553  opideq  38583  cnvref5  38591  raldmqseu  38605  ecun  38633  ecxrn  38646  disjressuc2  38651  disjecxrn  38652  disjecxrncnvep  38653  elrels5  38684  elrels6  38685  exeupre  38731  br2coss  38768  br1cossinres  38777  br1cossxrnres  38778  br1cossinidres  38779  br1cossincnvepres  38780  br1cossxrnidres  38781  br1cossxrncnvepres  38782  br1cosscnvxrn  38804  br1cossxrncnvssrres  38828  eldmqs1cossres  38984  erimeq2  39003  disjimdmqseq  39049  eldisjs7  39181  brabsb2  39227  prter3  39247  islshp  39344  islsat  39356  islshpat  39382  lcvexchlem1  39399  lsatnem0  39410  islfl  39425  ellkr  39454  lshpsmreu  39474  lshpkrlem3  39477  cvrval2  39639  cvrnbtwn2  39640  cvrnbtwn3  39641  isat  39651  leatb  39657  leat2  39659  cvlsupr2  39708  3dim0  39822  ps-2  39843  islln  39871  islln3  39875  llnexatN  39886  islpln  39895  islpln5  39900  lplnexatN  39928  islvol  39938  islvol5  39944  dalem-cly  40036  isline  40104  ispointN  40107  ispsubsp  40110  linepsubN  40117  elpmap  40123  isline4N  40142  elpadd  40164  paddcom  40178  pmapjoin  40217  pmapjat1  40218  llnexchb2  40234  elpclN  40257  pclcmpatN  40266  ispsubclN  40302  iswatN  40359  islhp  40361  islaut  40448  ispautN  40464  isldil  40475  isltrn  40484  isltrn2N  40485  isdilN  40519  istrnN  40522  cdlemefrs29bpre0  40761  cdleme40v  40834  istendo  41125  diaelval  41398  diaeldm  41401  dibopelvalN  41508  dibopelval2  41510  dib1dim  41530  dibglbN  41531  diblsmopel  41536  dicopelval  41542  dicelvalN  41543  dicelval3  41545  dicvalrelN  41550  diclspsn  41559  dihopelvalcpre  41613  xihopellsmN  41619  dihopellsm  41620  dih1  41651  dihglblem2aN  41658  dihglblem2N  41659  dihmeetlem4preN  41671  dihglb2  41707  dvh2dim  41810  islpolN  41848  lcfl7N  41866  lcdlss  41984  hdmap1fval  42161  hdmapfval  42192  hgmapfval  42251  hdmapglem7a  42292  hdmapoc  42296  lcmineqlem  42411  sn-iotalem  42582  cxpi11d  42702  fimgmcyclem  42892  fimgmcyc  42893  prjsperref  42953  isnacs  43050  mzpclval  43071  elmzpcl  43072  mzpcompact2lem  43097  eldiophb  43103  eldioph3  43112  fz1eqin  43115  diophrex  43121  eq0rabdioph  43122  rexrabdioph  43140  dvdsrabdioph  43156  eldioph4b  43157  eldioph4i  43158  elpell1qr  43193  elpell14qr  43195  elpell1234qr  43197  pell1234qrmulcl  43201  rmydioph  43360  rmxdioph  43362  aomclem8  43407  islmodfg  43415  islssfg2  43417  islnm2  43424  hbtlem2  43470  hbtlem5  43474  elmnc  43482  rngunsnply  43515  onsupmaxb  43585  orddif0suc  43614  onsucf1olem  43616  cantnf2  43671  tfsconcatb0  43690  tfsconcat0i  43691  tfsconcat00  43693  ofoafg  43700  oaun3lem1  43720  naddwordnexlem4  43747  fzunt  43800  fzuntd  43801  fzunt1d  43802  fzuntgd  43803  en2pr  43892  elmapintrab  43921  elinintrab  43922  brfvrcld  44036  brfvrcld2  44037  iunrelexpuztr  44064  brtrclfv2  44072  rfovcnvf1od  44349  fsovrfovd  44354  or3or  44368  ntrkbimka  44383  clsk3nimkb  44385  clsk1indlem4  44389  ntrclsiso  44412  ntrclskb  44414  ntrclsk3  44415  ntrclsk13  44416  ntrneiiso  44436  ntrneik2  44437  ntrneix2  44438  ntrneikb  44439  ntrneixb  44440  ntrneik3  44441  ntrneix3  44442  ntrneik13  44443  ntrneix13  44444  ntrneik4w  44445  gneispace3  44478  gneispace  44479  k0004lem1  44492  mnringmulrcld  44573  mnuunid  44622  grumnud  44631  expgrowth  44680  iotasbc2  44765  e2ebind  44908  modelaxreplem3  45325  modelac8prim  45337  permaxrep  45351  permac8prim  45359  nregmodel  45362  fvelrnbf  45367  rnmptbdd  45592  rnmptbd2  45596  rnmptbd  45603  caucvgbf  45836  lmbr3v  46092  lmbr3  46094  xlimpnfxnegmnf  46161  xlimmnf  46188  xlimpnf  46189  xlimmnfmpt  46190  xlimpnfmpt  46191  dfxlim2  46195  xlimpnfxnegmnf2  46205  cncfshiftioo  46239  itgiccshift  46327  itgperiod  46328  stoweidlem31  46378  stoweidlem34  46381  stoweidlem59  46406  fourierdlem2  46456  fourierdlem3  46457  fourierdlem42  46496  fourierdlem54  46507  fourierdlem81  46534  fourierdlem87  46540  fourierdlem92  46545  fourierdlem105  46558  fourierdlem113  46566  chnsubseqwl  47226  fsetsniunop  47398  fcoresf1ob  47422  f1ocof1ob  47430  reuf1odnf  47456  euoreqb  47458  fnopafvb  47504  afvelrnb  47512  afvelrnb0  47513  dmafv2rnb  47578  dfatopafv2b  47595  fnopafv2b  47598  fun2dmnopgexmpl  47633  2ffzoeq  47676  addmodne  47693  iccpart  47765  iccpartgt  47776  fargshiftfo  47791  ichexmpl2  47819  sprvalpw  47829  sprsymrelfvlem  47839  paireqne  47860  prprvalpw  47864  prprelb  47865  prprelprb  47866  prprsprreu  47868  prprreueq  47869  fmtnoprmfac1lem  47913  requad2  47972  fpprel  48077  fppr2odd  48080  nnsum3primesgbe  48141  bgoldbtbndlem3  48156  bgoldbtbnd  48158  vopnbgrel  48203  upgrimpths  48258  dfgric2  48264  grtriprop  48290  isgrtri  48292  stgredgel  48306  gpgvtxel  48396  gpgvtxedg1  48413  pgnbgreunbgrlem4  48468  pgnbgreunbgr  48474  isassintop  48559  assintopcllaw  48561  rngcinvALTV  48625  ringcinvALTV  48659  eliunxp2  48683  dmatALTbasel  48751  lcoval  48761  lco0  48776  lcoel0  48777  lindslinindsimp1  48806  lindslinindsimp2  48812  lincresunit3  48830  elbigo  48900  elbigo2  48901  nnolog2flm1  48939  rrx2pnedifcoorneor  49065  rrx2pnedifcoorneorr  49066  rrx2xpref1o  49067  rrx2line  49089  rrx2linest  49091  elrrx2linest2  49094  line2ylem  49100  line2x  49103  ralbidb  49148  ralbidc  49149  brab2dd  49176  resinsnALT  49221  ipolub  49336  ipoglb  49339  catprsc  49361  catprsc2  49362  funcf2lem  49429  0funcglem  49431  0funcg2  49432  0funclem  49434  termopropd  49592  fucofulem2  49659  isthincd2lem2  49783  functhinc  49796  thincsect  49815  2arwcatlem1  49943  setc1onsubc  49950