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  3323  cbvreu  3382  cbvrabwOLD  3426  cbvrab  3429  ceqsralt  3465  ralxpxfr2d  3589  clel2g  3602  clel4g  3606  elabd2  3613  ralab2  3644  rexab2  3646  reu7  3679  reu8  3680  2reu5  3705  ru  3727  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  ralss  3997  ralssOLD  3999  rexssOLD  4000  sbcssg  4462  rabsneq  4587  elpwunsn  4629  reuprg0  4647  reuprg  4648  prssg  4763  ssunsn2  4771  eqsn  4773  prneimg2  4799  preqsnd  4803  2ralunsn  4839  eluniab  4865  csbuni  4881  elintabg  4901  dfiin2g  4974  disjprg  5082  disjxun  5084  cbvopab1g  5161  cbvmptf  5186  cbvmptfg  5187  al0ssb  5243  reusv3  5340  elopg  5412  opthneg  5427  opeqsng  5449  sotrieq2  5562  frsn  5710  eliunxp  5784  exopxfr2  5791  relop  5797  eldm2g  5846  reldm0  5875  relrn0  5920  restidsing  6010  elimasng  6046  asymref2  6072  somin1  6088  imadifssran  6107  xpnz  6115  xpcan  6132  xpcan2  6133  relsn2  6168  dfpo2  6252  ordtri2  6350  ordtri3  6351  oneqmini  6368  cbviota  6455  iotaval2  6461  iota1  6469  sniota  6481  fncnv  6563  fnres  6617  sbcfng  6657  sbcfg  6658  brprcneu  6822  brprcneuALT  6823  fnopfvb  6883  fvelrnb  6892  funimass4  6896  unima  6907  dffv2  6927  fvopab3g  6934  eqfnfv  6975  eqfnfv3  6977  eqfnfv2f  6979  fvreseq0  6982  fnreseql  6992  fniniseg  7004  respreima  7010  rexrn  7031  ralrn  7032  f1ompt  7055  fssrescdmd  7071  fsn  7080  funopsn  7093  funsndifnop  7096  fprb  7140  tpres  7147  eufnfv  7175  ralima  7183  reximaOLD  7185  ralimaOLD  7186  dff13  7200  f13dfv  7220  fliftfun  7258  isocnv  7276  isoini  7284  f1oiso  7297  fnssintima  7308  imaeqsexvOLD  7309  cbvriota  7328  riotaeqimp  7341  eusvobj2  7350  oprabidw  7389  oprabid  7390  f1opr  7414  eloprabga  7467  resoprab  7476  eqfnov  7487  eqfnov2  7488  ov6g  7522  ovelrn  7534  funimassov  7535  ovelimab  7536  ndmovg  7541  caovord2  7570  imaeqexov  7596  imaeqalov  7597  tfisi  7801  eqop  7975  releldm2  7987  dfoprab4  7999  opiota  8003  bropopvvv  8031  bropfvvvv  8033  fparlem1  8053  fparlem2  8054  xporderlem  8068  poxp  8069  soxp  8070  fnwelem  8072  xpord2lem  8083  poxp2  8084  frxp2  8085  xpord2indlem  8088  poxp3  8091  frxp3  8092  xpord3pred  8093  xpord3inddlem  8095  elsuppfng  8110  elsuppfn  8111  rexsupp  8123  suppcoss  8148  mpoxopovel  8161  brtpos2  8173  brtpos0  8174  rntpos  8180  dftpos3  8185  tpostpos  8187  tpossym  8199  tposoprab  8203  mpocurryd  8210  frrlem1  8227  oevn0  8441  om00el  8502  omordlim  8503  omlimcl  8504  oeoa  8524  oeoe  8526  oeeulem  8528  oeeui  8529  oaabs2  8576  omabs  8578  cofonr  8601  naddunif  8620  naddasslem1  8621  naddasslem2  8622  erth2  8690  qliftfun  8740  erovlem  8751  ecopovsym  8757  mapdm0  8780  elpmg  8781  elpm2g  8782  dom2lem  8930  mapsnend  8974  xpdom2  9001  omxpenlem  9007  0sdomg  9035  fodomr  9057  xpf1o  9068  mapen  9070  ac6sfi  9185  fodomfir  9229  mapfien  9312  marypha2lem3  9341  ordtypelem7  9430  wemaplem1  9452  wemapsolem  9456  elharval  9467  brwdom3  9488  unwdomg  9490  xpwdomg  9491  inf3lem1  9538  cantnfs  9576  cantnfp1lem2  9589  cantnflem1d  9598  cantnflem1  9599  wemapwe  9607  ssttrcl  9625  ttrcltr  9626  ttrclss  9630  ttrclselem2  9636  r1sdom  9687  rankr1ai  9711  rankval2  9731  unbndrank  9755  rankunb  9763  tcrank  9797  bnd2  9806  cardnueq0  9877  iscard2  9889  r0weon  9923  fseqenlem1  9935  alephord2  9987  cardaleph  10000  aceq0  10029  dfac5lem4OLD  10039  dfac5  10040  kmlem14  10075  cfsmolem  10181  isfin4-2  10225  fin23lem26  10236  fin23lem22  10238  fin1a2lem7  10317  axdc3lem2  10362  axdc3  10365  zfac  10371  zornn0g  10416  axdclem  10430  brdom3  10439  zfcndac  10531  fpwwe2lem7  10549  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  pwfseqlem3  10572  winainflem  10605  eltsk2g  10663  inatsk  10690  axgroth2  10737  axgroth6  10740  sstskm  10754  ltexpi  10814  ordpinq  10855  lterpq  10882  ltanq  10883  ltmnq  10884  genpv  10911  genpelv  10912  prlem934  10945  prlem936  10959  addcmpblnr  10981  ltsrpr  10989  ltsosr  11006  mulgt0sr  11017  supsrlem  11023  elreal2  11044  ltresr  11052  ltresr2  11053  axrrecex  11075  axpre-ltadd  11079  axpre-mulgt0  11080  axpre-sup  11081  subcan2  11408  negcon1  11435  negcon2  11436  lt0neg1  11645  lt0neg2  11646  le0neg1  11647  le0neg2  11648  msq0d  11789  mulcan2g  11793  divmul2  11802  reclt1  12040  recgt1  12041  infm3  12104  suprlub  12109  suprleub  12111  infregelb  12129  ind1a  12159  addltmul  12402  arch  12423  elznn0  12528  nn0lt2  12581  eluz1  12781  raluz  12835  rexuz  12837  nnwof  12853  cnref1o  12924  ltxr  13055  xrltlen  13086  dflt2  13088  xrrebnd  13109  xlt0neg1  13160  xlt0neg2  13161  xle0neg1  13162  xle0neg2  13163  xmulneg1  13210  supxrbnd  13269  elixx1  13296  ixxun  13303  elioo2  13328  elicc4  13355  elioopnf  13385  elioomnf  13386  iccneg  13414  iccshftr  13428  iccshftl  13430  iccdil  13432  icccntr  13434  iccf1o  13438  elfz1  13455  0fz1  13487  elfzp1  13517  fzpr  13522  uzsplit  13539  elfzm1b  13545  elfzp12  13546  fznn0  13562  fvinim0ffz  13733  injresinj  13735  fleqceilz  13802  zmodid2  13847  fsuppmapnn0fiub0  13944  bernneq  14180  hasheqf1o  14300  euhash1  14371  hashbclem  14403  hashfacen  14405  hashf1  14408  hashge2el2difr  14432  hashtpg  14436  ccatrn  14541  pfxsuffeqwrdeq  14649  wrd2ind  14674  scshwfzeqfzo  14777  wwlktovf1  14908  brtrclfv  14953  2shfti  15031  sqrtmsq2i  15339  limsupgle  15428  limsuple  15429  rlim  15446  clim0  15457  ello12  15467  elo12  15478  o1lo1  15488  rlimresb  15516  lo1add  15578  lo1mul  15579  rlimno1  15605  summo  15668  fsumsplit  15692  mertenslem2  15839  prodmo  15890  fprodsplit  15920  fprod2dlem  15934  cnso  16203  sqrt2irr  16205  dvdsval2  16213  alzdvds  16278  odd2np1lem  16298  even2n  16300  sumodd  16346  divalgb  16362  divalgmod  16364  bitsval  16382  bitsmod  16394  sadcp1  16413  gcddvds  16461  bezoutlem3  16499  bezout  16501  lcmfunsnlem2  16598  isprm3  16641  prmind2  16643  dvdsprime  16645  ge2nprmge4  16660  coprm  16670  prmdvdsexp  16674  crth  16737  pythagtriplem2  16777  pythagtrip  16794  pceu  16806  pc11  16840  vdwapval  16933  vdwapun  16934  vdwlem10  16950  vdwlem12  16952  vdwlem13  16953  ramval  16968  ramub1lem2  16987  prmlem0  17065  elrest  17379  imasleval  17494  ismri  17586  isacs  17606  isacs2  17608  acsfn1  17616  iscatd2  17636  homfeq  17649  catpropd  17664  ismon  17689  issect  17709  issect2  17710  isinv  17716  cic  17755  isssc  17776  isfunc  17820  funcres2b  17853  isnat  17906  fucinv  17932  iszeroo  17954  elhoma  17988  setcinv  18046  isprs  18251  isdrs  18256  lubeldm  18306  glbeldm  18319  istos  18371  tosso  18372  latnle  18428  latdisd  18452  isdlat  18477  isipodrs  18492  isacs5  18503  chnccat  18581  ismgmhm  18653  issubmgm  18659  ismhm  18742  issubm  18760  issubmndb  18762  sursubmefmnd  18853  injsubmefmnd  18854  grpsubeq0  18991  grpsubadd  18993  issubg  19091  subgmulg  19105  issubg3  19109  isnsg  19119  eqger  19142  eqglact  19143  eqgid  19144  cycsubmel  19164  isghm  19179  isghmOLD  19180  isga  19255  gacan  19269  gaorb  19271  gastacos  19274  orbsta  19277  elcntz  19286  elcntzsn  19289  sscntz  19290  gsmsymgreq  19396  psgnunilem5  19458  psgnunilem3  19460  psgneldm2  19468  psgneu  19470  psgnfitr  19481  dfod2  19528  isslw  19572  sylow2alem2  19582  lsmelvalx  19604  lsmcom2  19619  lsmass  19633  lssnle  19638  pj1eu  19660  lsmhash  19669  efgi  19683  efgval2  19688  efgtlen  19690  efgred  19712  lsmcomx  19820  iscyggen2  19845  iscyg3  19850  gsumval3eu  19868  gsumzsplit  19891  eldprd  19970  subgdmdprd  20000  dprddisj2  20005  dprd2da  20008  dmdprdsplit2lem  20011  dmdprdsplit2  20012  dprdsplit  20014  dmdprdpr  20015  pgpfac1lem3  20043  pgpfac1lem4  20044  pgpfac1lem5  20045  srgfcl  20166  dvdsr02  20341  isunit  20342  isirred  20388  isrnghmmul  20411  isrngim  20414  c0snmgmhm  20431  isrhm  20447  isrim0  20451  isnzr2  20484  0ringnnzr  20491  subsubrng2  20530  subsubrg2  20565  issubrg3  20566  rngcinv  20603  ringcinv  20637  isdomn3  20681  drngunit  20700  issdrg  20754  isabv  20777  islmod  20848  islss  20918  ellspsn  20987  islmhm  21012  lmhmeql  21040  islbs  21061  lsmspsn  21069  lsmelval2  21070  lspprel  21079  lvecvscan2  21100  lvecinv  21101  lspsneq  21110  lspsneu  21111  lspsolvlem  21130  islpidl  21313  lidldvgen  21322  prmirredlem  21460  zrhrhmb  21498  zndvds  21537  elocv  21656  iscss  21671  pjdm  21695  ishil2  21707  isobs  21708  obslbs  21718  frlmelbas  21744  ellspd  21790  islinds  21797  islindf4  21826  aspval2  21886  mplsubglem  21986  mpllsslem  21987  mplmonmul  22023  opsrtoslem2  22043  ismhp  22115  mat1dimelbas  22445  dmatel  22467  scmatel  22479  mdetunilem8  22593  mdetunilem9  22594  maducoeval2  22614  cramer0  22664  cpmatel  22685  istop2g  22870  istopon  22886  toprntopon  22899  isbasis2g  22922  isbasis3g  22923  tgss2  22961  bastop1  22967  iscld  23001  elcls  23047  ntreq0  23051  isclo  23061  isclo2  23062  islp  23114  lpdifsn  23117  islpi  23123  restsn  23144  restlp  23157  ordtbaslem  23162  ordtbas2  23165  lmbr  23232  cnprest2  23264  ist0-3  23319  ist1-2  23321  cmpsublem  23373  cmpfi  23382  1stcrest  23427  2ndcdisj  23430  1stccnp  23436  llyi  23448  nllyi  23449  lly1stc  23470  iskgen3  23523  kgencn  23530  txbas  23541  eltx  23542  elpt  23546  xkoccn  23593  ptcnplem  23595  hausdiag  23619  hauseqlcld  23620  txlm  23622  txkgen  23626  kqfvima  23704  kqt0lem  23710  r0cld  23712  regr1lem2  23714  hmeoimaf1o  23744  isfbas2  23809  fbssfi  23811  trfbas2  23817  trfil2  23861  fmfnfmlem4  23931  elflim2  23938  flimrest  23957  cnflf  23976  txflf  23980  fclsopn  23988  ufilcmp  24006  cnfcf  24016  alexsubALTlem4  24024  cnextf  24040  tmdcn2  24063  qustgpopn  24094  qustgplem  24095  eltsms  24107  tsmsgsum  24113  tsmssplit  24126  elutop  24207  ustuqtop  24220  utopsnneiplem  24221  isusp  24235  isucn  24251  iscfilu  24261  ispsmet  24278  ismet  24297  isxmet  24298  metn0  24334  elblps  24361  elbl  24362  metrest  24498  metuel2  24539  psmetutop  24541  restmetu  24544  dscmet  24546  nrmmetd  24548  isngp3  24572  nmogelb  24690  isnmhm  24720  qtopbaslem  24732  xrsxmet  24784  icccmplem2  24798  metdseq0  24829  elcncf  24865  cnheibor  24931  ishtpy  24948  isphtpy  24957  isphtpc  24970  om1elbas  25008  elpi1  25021  isclmp  25073  nmhmcn  25096  iscph  25146  tcphcph  25213  lmmbrf  25238  iscfil  25241  iscfil2  25242  iscau  25252  caucfil  25259  iscmet  25260  iscmet3  25269  cfilucfil3  25296  bcthlem1  25300  rrxcph  25368  minveclem3b  25404  minveclem6  25410  evthicc2  25436  ovolfioo  25443  ovolficc  25444  ovolshftlem1  25485  ovolscalem1  25489  iundisj2  25525  dyadmbl  25576  volsup2  25581  mbfmax  25625  mbfsup  25640  mbfinf  25641  i1f1lem  25665  i1fres  25681  itg1climres  25690  itg2leub  25710  itg2seq  25718  itg2splitlem  25724  itg2monolem1  25726  itg2mono  25729  itg2cn  25739  iblpos  25769  iblcn  25775  itgsplit  25812  ellimc2  25853  dvreslem  25885  elcpn  25910  rolle  25966  dvlip  25970  dvivth  25987  tdeglem4  26037  mdegleb  26041  deg1ldg  26069  ply1nzb  26100  ply1divmo  26113  ply1divex  26114  fta1glem2  26146  plyco0  26169  elply  26172  coeeu  26202  plydivex  26276  taylthlem2  26353  taylthlem2OLD  26354  radcnvlt1  26398  sincosq1sgn  26478  sincosq2sgn  26479  coseq1  26505  logreclem  26743  affineequiv  26804  affineequiv4  26807  dcubic  26827  quart  26842  atans2  26912  efrlim  26950  efrlimOLD  26951  mumullem2  27161  dvdsflsumcom  27169  fsumvma2  27196  chpchtsum  27201  chpub  27202  dchrelbas  27218  dchrelbas2  27219  dchreq  27240  dchrptlem2  27247  gausslemma2dlem0i  27346  lgsquadlem2  27363  m1lgs  27370  2lgsoddprmlem3  27396  2sqlem6  27405  2sqlem9  27409  2sqlem10  27410  2sq2  27415  2sqreunnltb  27443  2sqreuop  27444  2sqreuopnn  27445  2sqreuoplt  27446  2sqreuopltb  27447  2sqreuopnnlt  27448  2sqreuopnnltb  27449  2sqreuopb  27450  dchrisum0flb  27492  pntpbnd1  27568  pntlem3  27591  pntlemp  27592  ltsval2  27639  ltsintdifex  27644  ltsres  27645  noextenddif  27651  nosepssdm  27669  nosupprefixmo  27683  noinfprefixmo  27684  nosupcbv  27685  nosupno  27686  nosupbnd1lem1  27691  noinfcbv  27700  noinfno  27701  noinfdm  27702  noinfres  27705  noinfbnd1lem1  27706  lestri3  27738  cutbdaylt  27809  ltsrec  27812  elold  27870  sltsleft  27871  sltsright  27872  madebdayim  27899  madebdaylemlrcut  27910  madebday  27911  newbday  27913  ltslpss  27919  cofcutr  27935  cofcutrtime  27938  addsval2  27974  addsrid  27975  addsprop  27987  negsprop  28046  lt0negs2d  28062  subadds  28081  mulsval2lem  28121  mulsrid  28124  mulsprop  28141  mulscom  28150  mulsunif2  28181  mulscan2d  28190  precsexlemcbv  28217  precsexlem9  28226  recsex  28230  absnegs  28258  onsfi  28367  n0lts1e0  28379  bdayn0p1  28380  bdayn0sf1o  28381  dfnns2  28383  eucliddivs  28387  elnnzs  28412  elznns  28413  n0seo  28432  pw2recs  28449  avglts1d  28464  avglts2d  28465  bdaypw2n0bndlem  28474  bdayfinbndcbv  28477  bdayfinbndlem1  28478  bdayfinbndlem2  28479  z12bdaylem1  28481  z12zsodd  28493  z12bday  28496  bdayfin  28498  recut  28505  renegscl  28509  remulscl  28513  istrkg2ld  28547  iscgrg  28599  tgcgr4  28618  isismt  28621  tgellng  28640  tgcolg  28641  legov  28672  lnhl  28702  lmimid  28881  iscgra1  28897  ttgelitv  28970  elee  28981  mpteleeOLD  28983  colinearalglem2  28995  colinearalg  28998  ax5seglem5  29021  axeuclidlem  29050  axeuclid  29051  axcontlem1  29052  axcontlem2  29053  axcontlem5  29056  axcontlem7  29058  wrdupgr  29173  wrdumgr  29185  uhgrspansubgrlem  29378  nbgrel  29428  nbupgrel  29433  nbgr2vtx1edg  29438  nbuhgr2vtx1edgblem  29439  nbuhgr2vtx1edgb  29440  nb3grprlem2  29469  nb3grpr2  29471  uvtx01vtx  29485  uvtxusgrel  29491  iscplgr  29503  vtxdun  29570  fusgrn0degnn0  29588  1loopgrnb0  29591  umgr2v2enb1  29615  vdiscusgrb  29619  wlkl1loop  29726  wlkv0  29738  wlklenvclwlk  29742  upgr2wlk  29755  wlkp1lem8  29767  upgrtrls  29788  upgristrl  29789  dfpth2  29817  isspthonpth  29837  usgr2trlncl  29848  usgr2pthlem  29851  usgr2pth  29852  pthdlem1  29854  isclwlke  29865  isclwlkupgr  29866  uspgrn2crct  29896  wwlks  29923  iswwlksn  29926  wwlksnext  29981  wwlksnextinj  29987  wspn0  30012  wpthswwlks2on  30052  rusgrnumwwlkl1  30059  rusgrnumwwlkslem  30060  rusgrnumwwlkb0  30062  clwlkclwwlk  30092  clwwlknwwlksn  30128  clwwlkn2  30134  clwwlkel  30136  clwwlkwwlksb  30144  hashecclwwlkn1  30167  umgrhashecclwwlk  30168  clwwlknon1loop  30188  0wlk  30206  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  dfconngr1  30278  vdn0conngrumgrv2  30286  eupth2lem2  30309  eupth2lem3lem6  30323  eucrct2eupth  30335  isfrgr  30350  frgr3v  30365  frgrncvvdeqlem3  30391  frgrncvvdeqlem6  30394  frgrwopreglem2  30403  fusgreg2wsplem  30423  2clwwlkel  30439  extwwlkfabel  30443  numclwwlk1lem2f1  30447  numclwwlk1lem2fo  30448  numclwwlk2lem1  30466  numclwlk2lem2f  30467  numclwlk2lem2f1o  30469  nrt2irr  30563  isgrpo  30588  isssp  30815  islno  30844  nmogtmnf  30861  nmoubi  30863  nmounbi  30867  isblo  30873  ishmo  30902  ubthlem1  30961  ubthlem2  30962  minvecolem5  30972  minvecolem6  30973  hvmulcan2  31164  hire  31185  ocel  31372  ocsh  31374  pjhthmo  31393  shscom  31410  shmodsi  31480  elspani  31634  adjsym  31924  eigorthi  31928  nmopgtmnf  31959  adjeu  31980  adjval2  31982  cnvadj  31983  nmopub  31999  nmfnleub  32016  eleigvec  32048  nmop0h  32082  largei  32358  mdbr2  32387  mddmd2  32400  mdsl2i  32413  chrelat3  32462  atnemeq0  32468  chirredlem1  32481  sumdmdii  32506  sumdmdlem  32509  dmdbr5ati  32513  cdjreui  32523  nelun  32603  tpssg  32627  disjabrex  32672  disjabrexf  32673  iundisj2f  32680  disjunsn  32684  brab2d  32698  br8d  32701  opabdm  32704  opabrn  32705  nfpconfp  32725  ofpreima  32758  funcnv5mpt  32760  suppiniseg  32779  1stpreima  32800  curry2ima  32802  f1od2  32812  fpwrelmap  32826  infxrge0gelb  32859  xnn01gt  32863  nndiffz1  32879  iundisj2fi  32890  fzo0opth  32896  sgn3da  32927  tlt3  33050  toslublem  33052  tosglblem  33054  ismnt  33063  cntzun  33160  isfxp  33249  isarchi2  33266  erler  33346  domnprodeq0  33357  qusker  33429  unitprodclb  33469  lsmsnorb  33471  lsmssass  33482  grplsm0l  33483  isprmidl  33518  ismxidl  33542  mxidlirred  33552  isrprm  33597  ufdprmidl  33621  1arithufdlem4  33627  ply1degltel  33674  ply1degleel  33675  psrmonmul  33714  vieta  33744  elirng  33851  algextdeglem8  33889  fldext2chn  33893  constrextdg2  33914  constrfiss  33916  smatrcl  33961  zarcls  34039  rhmpreimacnlem  34049  cnvordtrestixx  34078  ordtconnlem1  34089  fsumcvg4  34115  lmdvg  34118  esum2dlem  34257  braew  34407  ismbfm  34416  mbfmcnt  34433  issibf  34498  eulerpartgbij  34537  eulerpartlemgvv  34541  eulerpartlemgh  34543  elorvc  34625  ballotlemfc0  34658  ballotlemfcc  34659  ballotlemodife  34663  reprinrn  34783  reprdifc  34792  bnj1366  34992  bnj984  35115  bnj1171  35163  bnj1253  35180  bnj1417  35204  bnj1452  35215  rankval2b  35263  axprALT2  35274  lfuhgr3  35323  subfacp1lem3  35385  subfacp1lem5  35387  subfacp1lem6  35388  erdszelem9  35402  erdszelem10  35403  erdsze2lem2  35407  iscvm  35462  cvmlift2lem10  35515  snmlval  35534  satfv1  35566  satfvsucsuc  35568  satfrnmapom  35573  satf0op  35580  satf0n0  35581  sat1el2xp  35582  fmlafvel  35588  fmlaomn0  35593  gonarlem  35597  fmla0disjsuc  35601  fmlasucdisj  35602  satffunlem1lem1  35605  satffunlem2lem1  35607  satefvfmla0  35621  sategoelfvb  35622  mclsppslem  35786  r1peuqusdeg1  35846  climuzcnv  35874  br6  35960  elintfv  35968  dfdm5  35976  dfrn5  35977  dfon2lem7  35990  dfon2  35993  dfrdg2  35996  elfuns  36116  dfiota3  36124  brimg  36138  dfrdg4  36154  btwnouttr  36227  btwnexch  36228  funtransport  36234  cgr3permute1  36251  colinearperm1  36265  brsegle  36311  outsideoftr  36332  outsideofeu  36334  funray  36343  funline  36345  lineunray  36350  lineelsb2  36351  nn0prpwlem  36525  nn0prpw  36526  fneval  36555  topfneec  36558  filnetlem4  36584  ordcmp  36650  regsfromregtco  36741  regsfromsetind  36742  bj-sblem  37164  bj-sbceqgALT  37222  bj-elgab  37259  bj-clel3gALT  37368  bj-restpw  37417  bj-elid6  37497  bj-eldiag  37503  bj-eldiag2  37504  bj-imdirco  37517  f1omptsnlem  37663  mptsnunlem  37665  topdifinfeq  37677  isbasisrelowllem1  37682  isbasisrelowllem2  37683  relowlpssretop  37691  fvineqsnf1  37737  fvineqsneu  37738  wl-ifpimpr  37793  wl-sbcom2d  37897  wl-sbalnae  37898  curf  37930  unccur  37935  phpreu  37936  finixpnum  37937  ptrest  37951  poimirlem8  37960  poimirlem17  37969  poimirlem18  37970  poimirlem20  37972  poimirlem21  37973  poimirlem23  37975  poimirlem26  37978  poimirlem27  37979  poimirlem28  37980  poimirlem31  37983  poimirlem32  37984  poimir  37985  heicant  37987  mblfinlem1  37989  ismblfin  37993  mbfresfi  37998  itg2addnclem  38003  itg2addnclem2  38004  itg2addnc  38006  itg2gt0cn  38007  ftc1anclem6  38030  unirep  38046  indexa  38065  sdclem1  38075  fdc  38077  neificl  38085  istotbnd  38101  sstotbnd2  38106  isbnd  38112  isbnd3b  38117  heibor1lem  38141  heiborlem3  38145  rrnheibor  38169  ismgmOLD  38182  rngosn3  38256  isrngohom  38297  isrngoiso  38310  iscrngo2  38329  isidl  38346  ispridl  38366  pridlidl  38367  pridlnr  38368  pridl  38369  ismaxidl  38372  maxidlidl  38373  smprngopr  38384  prnc  38399  eldmres  38609  eldmressnALTV  38611  eldmqsres  38625  ideq2  38645  opideq  38675  cnvref5  38683  raldmqseu  38697  ecun  38725  ecxrn  38738  disjressuc2  38743  disjecxrn  38744  disjecxrncnvep  38745  elrels5  38776  elrels6  38777  exeupre  38823  br2coss  38860  br1cossinres  38869  br1cossxrnres  38870  br1cossinidres  38871  br1cossincnvepres  38872  br1cossxrnidres  38873  br1cossxrncnvepres  38874  br1cosscnvxrn  38896  br1cossxrncnvssrres  38920  eldmqs1cossres  39076  erimeq2  39095  disjimdmqseq  39141  eldisjs7  39273  brabsb2  39319  prter3  39339  islshp  39436  islsat  39448  islshpat  39474  lcvexchlem1  39491  lsatnem0  39502  islfl  39517  ellkr  39546  lshpsmreu  39566  lshpkrlem3  39569  cvrval2  39731  cvrnbtwn2  39732  cvrnbtwn3  39733  isat  39743  leatb  39749  leat2  39751  cvlsupr2  39800  3dim0  39914  ps-2  39935  islln  39963  islln3  39967  llnexatN  39978  islpln  39987  islpln5  39992  lplnexatN  40020  islvol  40030  islvol5  40036  dalem-cly  40128  isline  40196  ispointN  40199  ispsubsp  40202  linepsubN  40209  elpmap  40215  isline4N  40234  elpadd  40256  paddcom  40270  pmapjoin  40309  pmapjat1  40310  llnexchb2  40326  elpclN  40349  pclcmpatN  40358  ispsubclN  40394  iswatN  40451  islhp  40453  islaut  40540  ispautN  40556  isldil  40567  isltrn  40576  isltrn2N  40577  isdilN  40611  istrnN  40614  cdlemefrs29bpre0  40853  cdleme40v  40926  istendo  41217  diaelval  41490  diaeldm  41493  dibopelvalN  41600  dibopelval2  41602  dib1dim  41622  dibglbN  41623  diblsmopel  41628  dicopelval  41634  dicelvalN  41635  dicelval3  41637  dicvalrelN  41642  diclspsn  41651  dihopelvalcpre  41705  xihopellsmN  41711  dihopellsm  41712  dih1  41743  dihglblem2aN  41750  dihglblem2N  41751  dihmeetlem4preN  41763  dihglb2  41799  dvh2dim  41902  islpolN  41940  lcfl7N  41958  lcdlss  42076  hdmap1fval  42253  hdmapfval  42284  hgmapfval  42343  hdmapglem7a  42384  hdmapoc  42388  lcmineqlem  42502  sn-iotalem  42673  cxpi11d  42786  redivmul2d  42889  fimgmcyclem  42989  fimgmcyc  42990  prjsperref  43050  isnacs  43147  mzpclval  43168  elmzpcl  43169  mzpcompact2lem  43194  eldiophb  43200  eldioph3  43209  fz1eqin  43212  diophrex  43218  eq0rabdioph  43219  rexrabdioph  43237  dvdsrabdioph  43253  eldioph4b  43254  eldioph4i  43255  elpell1qr  43290  elpell14qr  43292  elpell1234qr  43294  pell1234qrmulcl  43298  rmydioph  43457  rmxdioph  43459  aomclem8  43504  islmodfg  43512  islssfg2  43514  islnm2  43521  hbtlem2  43567  hbtlem5  43571  elmnc  43579  rngunsnply  43612  onsupmaxb  43682  orddif0suc  43711  onsucf1olem  43713  cantnf2  43768  tfsconcatb0  43787  tfsconcat0i  43788  tfsconcat00  43790  ofoafg  43797  oaun3lem1  43817  naddwordnexlem4  43844  fzunt  43897  fzuntd  43898  fzunt1d  43899  fzuntgd  43900  en2pr  43989  elmapintrab  44018  elinintrab  44019  brfvrcld  44133  brfvrcld2  44134  iunrelexpuztr  44161  brtrclfv2  44169  rfovcnvf1od  44446  fsovrfovd  44451  or3or  44465  ntrkbimka  44480  clsk3nimkb  44482  clsk1indlem4  44486  ntrclsiso  44509  ntrclskb  44511  ntrclsk3  44512  ntrclsk13  44513  ntrneiiso  44533  ntrneik2  44534  ntrneix2  44535  ntrneikb  44536  ntrneixb  44537  ntrneik3  44538  ntrneix3  44539  ntrneik13  44540  ntrneix13  44541  ntrneik4w  44542  gneispace3  44575  gneispace  44576  k0004lem1  44589  mnringmulrcld  44670  mnuunid  44719  grumnud  44728  expgrowth  44777  iotasbc2  44862  e2ebind  45005  modelaxreplem3  45422  modelac8prim  45434  permaxrep  45448  permac8prim  45456  nregmodel  45459  fvelrnbf  45464  rnmptbdd  45689  rnmptbd2  45693  rnmptbd  45700  caucvgbf  45932  lmbr3v  46188  lmbr3  46190  xlimpnfxnegmnf  46257  xlimmnf  46284  xlimpnf  46285  xlimmnfmpt  46286  xlimpnfmpt  46287  dfxlim2  46291  xlimpnfxnegmnf2  46301  cncfshiftioo  46335  itgiccshift  46423  itgperiod  46424  stoweidlem31  46474  stoweidlem34  46477  stoweidlem59  46502  fourierdlem2  46552  fourierdlem3  46553  fourierdlem42  46592  fourierdlem54  46603  fourierdlem81  46630  fourierdlem87  46636  fourierdlem92  46641  fourierdlem105  46654  fourierdlem113  46662  chnsubseqwl  47322  fsetsniunop  47494  fcoresf1ob  47518  f1ocof1ob  47526  reuf1odnf  47552  euoreqb  47554  fnopafvb  47600  afvelrnb  47608  afvelrnb0  47609  dmafv2rnb  47674  dfatopafv2b  47691  fnopafv2b  47694  fun2dmnopgexmpl  47729  2ffzoeq  47773  addmodne  47795  iccpart  47873  iccpartgt  47884  fargshiftfo  47899  ichexmpl2  47927  sprvalpw  47937  sprsymrelfvlem  47947  paireqne  47968  prprvalpw  47972  prprelb  47973  prprelprb  47974  prprsprreu  47976  prprreueq  47977  nprmmul3  47986  fmtnoprmfac1lem  48024  requad2  48096  fpprel  48201  fppr2odd  48204  nnsum3primesgbe  48265  bgoldbtbndlem3  48280  bgoldbtbnd  48282  vopnbgrel  48327  upgrimpths  48382  dfgric2  48388  grtriprop  48414  isgrtri  48416  stgredgel  48430  gpgvtxel  48520  gpgvtxedg1  48537  pgnbgreunbgrlem4  48592  pgnbgreunbgr  48598  isassintop  48683  assintopcllaw  48685  rngcinvALTV  48749  ringcinvALTV  48783  eliunxp2  48807  dmatALTbasel  48875  lcoval  48885  lco0  48900  lcoel0  48901  lindslinindsimp1  48930  lindslinindsimp2  48936  lincresunit3  48954  elbigo  49024  elbigo2  49025  nnolog2flm1  49063  rrx2pnedifcoorneor  49189  rrx2pnedifcoorneorr  49190  rrx2xpref1o  49191  rrx2line  49213  rrx2linest  49215  elrrx2linest2  49218  line2ylem  49224  line2x  49227  ralbidb  49272  ralbidc  49273  brab2dd  49300  resinsnALT  49345  ipolub  49460  ipoglb  49463  catprsc  49485  catprsc2  49486  funcf2lem  49553  0funcglem  49555  0funcg2  49556  0funclem  49558  termopropd  49716  fucofulem2  49783  isthincd2lem2  49907  functhinc  49920  thincsect  49939  2arwcatlem1  50067  setc1onsubc  50074