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 205

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 206

This theorem is referenced by:  bitr2di  288  bitr4di  289  3bitr3g  313  bibi2i  337  ibibr  368  biancomd  463  pm5.75  1027  19.17  2215  sb2ae  2491  sbcom3  2501  sbal1  2523  sbal2  2524  eqabrd  2872  cbvralfwOLD  3317  cbvralf  3353  cbvreuwOLD  3409  cbvreu  3421  cbvrabw  3464  cbvrab  3470  ceqsralt  3504  ralxpxfr2d  3632  clel2g  3645  clel4g  3650  elabd2  3658  ralab2  3692  rexab2  3694  reu7  3727  reu8  3728  2reu5  3753  cbvralcsf  3937  cbvreucsf  3939  cbvrabcsf  3940  ralss  4052  rexss  4053  sbcssg  4524  elpwunsn  4688  reuprg0  4707  reuprg  4708  prssg  4823  ssunsn2  4831  eqsn  4833  preqsnd  4860  2ralunsn  4896  eluniab  4922  csbuni  4939  elintabg  4960  elintabOLD  4962  dfiun2gOLD  5034  dfiin2g  5035  disjprgw  5143  disjprg  5144  disjxun  5146  cbvopab1g  5224  cbvmptf  5257  cbvmptfg  5258  al0ssb  5308  reusv3  5405  elopg  5468  opthneg  5483  opeqsng  5505  sotrieq2  5620  frsn  5765  eliunxp  5840  exopxfr2  5847  relop  5853  eldm2g  5902  reldm0  5930  relrn0  5972  restidsing  6056  elimasng  6092  asymref2  6123  somin1  6139  xpnz  6163  xpcan  6180  xpcan2  6181  relsn2  6216  dfpo2  6300  ordtri2  6404  ordtri3  6405  oneqmini  6421  cbviota  6510  iotaval2  6516  iotavalOLD  6522  iota1  6525  sniota  6539  fncnv  6626  fnres  6682  sbcfng  6719  sbcfg  6720  brprcneu  6887  brprcneuALT  6888  fnopfvb  6951  fvelrnb  6959  funimass4  6963  unima  6973  dffv2  6993  fvopab3g  7000  eqfnfv  7040  eqfnfv3  7042  eqfnfv2f  7044  fvreseq0  7047  fnreseql  7057  fniniseg  7069  respreima  7075  rexrn  7097  ralrn  7098  f1ompt  7121  fsn  7144  funopsn  7157  funsndifnop  7160  fprb  7206  tpres  7213  eufnfv  7241  rexima  7249  ralima  7250  dff13  7265  f13dfv  7283  fliftfun  7320  isocnv  7338  isoini  7346  f1oiso  7359  fnssintima  7370  imaeqsexv  7371  cbvriota  7390  riotaeqimp  7403  eusvobj2  7412  oprabidw  7451  oprabid  7452  f1opr  7476  eloprabga  7528  eloprabgaOLD  7529  resoprab  7538  eqfnov  7550  eqfnov2  7551  ov6g  7585  ovelrn  7597  funimassov  7598  ovelimab  7599  ndmovg  7604  caovord2  7633  imaeqexov  7659  imaeqalov  7660  tfisi  7863  eqop  8035  releldm2  8047  dfoprab4  8059  opiota  8063  bropopvvv  8095  bropfvvvv  8097  fparlem1  8117  fparlem2  8118  xporderlem  8132  poxp  8133  soxp  8134  fnwelem  8136  xpord2lem  8147  poxp2  8148  frxp2  8149  xpord2indlem  8152  poxp3  8155  frxp3  8156  xpord3pred  8157  xpord3inddlem  8159  elsuppfng  8174  elsuppfn  8175  rexsupp  8186  suppcoss  8212  mpoxopovel  8225  brtpos2  8237  brtpos0  8238  rntpos  8244  dftpos3  8249  tpostpos  8251  tpossym  8263  tposoprab  8267  mpocurryd  8274  frrlem1  8291  wfrlem1OLD  8328  oevn0  8535  om00el  8596  omordlim  8597  omlimcl  8598  oeoa  8617  oeoe  8619  oeeulem  8621  oeeui  8622  oaabs2  8669  omabs  8671  cofonr  8694  naddunif  8713  naddasslem1  8714  naddasslem2  8715  erth2  8775  qliftfun  8820  erovlem  8831  ecopovsym  8837  mapdm0  8860  elpmg  8861  elpm2g  8862  dom2lem  9012  mapsnend  9060  xpdom2  9091  omxpenlem  9097  0sdomg  9128  0sdomgOLD  9129  fodomr  9152  xpf1o  9163  mapen  9165  ac6sfi  9311  mapfien  9431  marypha2lem3  9460  ordtypelem7  9547  wemaplem1  9569  wemapsolem  9573  elharval  9584  brwdom3  9605  unwdomg  9607  xpwdomg  9608  inf3lem1  9651  cantnfs  9689  cantnfp1lem2  9702  cantnflem1d  9711  cantnflem1  9712  wemapwe  9720  ssttrcl  9738  ttrcltr  9739  ttrclss  9743  ttrclselem2  9749  r1sdom  9797  rankr1ai  9821  rankval2  9841  unbndrank  9865  rankunb  9873  tcrank  9907  bnd2  9916  cardnueq0  9987  iscard2  9999  r0weon  10035  fseqenlem1  10047  alephord2  10099  cardaleph  10112  aceq0  10141  dfac5lem4  10149  dfac5  10151  kmlem14  10186  cfsmolem  10293  isfin4-2  10337  fin23lem26  10348  fin23lem22  10350  fin1a2lem7  10429  axdc3lem2  10474  axdc3  10477  zfac  10483  zornn0g  10528  axdclem  10542  brdom3  10551  zfcndac  10642  fpwwe2lem7  10660  fpwwe2lem11  10664  fpwwe2lem12  10665  fpwwe2  10666  pwfseqlem3  10683  winainflem  10716  eltsk2g  10774  inatsk  10801  axgroth2  10848  axgroth6  10851  sstskm  10865  ltexpi  10925  ordpinq  10966  lterpq  10993  ltanq  10994  ltmnq  10995  genpv  11022  genpelv  11023  prlem934  11056  prlem936  11070  addcmpblnr  11092  ltsrpr  11100  ltsosr  11117  mulgt0sr  11128  supsrlem  11134  elreal2  11155  ltresr  11163  ltresr2  11164  axrrecex  11186  axpre-ltadd  11190  axpre-mulgt0  11191  axpre-sup  11192  subcan2  11515  negcon1  11542  negcon2  11543  lt0neg1  11750  lt0neg2  11751  le0neg1  11752  le0neg2  11753  msq0d  11893  mulcan2g  11898  divmul2  11906  reclt1  12139  recgt1  12140  infm3  12203  suprlub  12208  suprleub  12210  infregelb  12228  addltmul  12478  arch  12499  elznn0  12603  nn0lt2  12655  eluz1  12856  raluz  12910  rexuz  12912  nnwof  12928  cnref1o  12999  ltxr  13127  xrltlen  13157  dflt2  13159  xrrebnd  13179  xlt0neg1  13230  xlt0neg2  13231  xle0neg1  13232  xle0neg2  13233  xmulneg1  13280  supxrbnd  13339  elixx1  13365  ixxun  13372  elioo2  13397  elicc4  13423  elioopnf  13452  elioomnf  13453  iccneg  13481  iccshftr  13495  iccshftl  13497  iccdil  13499  icccntr  13501  iccf1o  13505  elfz1  13521  0fz1  13553  elfzp1  13583  fzpr  13588  uzsplit  13605  elfzm1b  13611  elfzp12  13612  fznn0  13625  fvinim0ffz  13783  injresinj  13785  fleqceilz  13851  zmodid2  13896  fsuppmapnn0fiub0  13990  bernneq  14223  hasheqf1o  14340  euhash1  14411  hashbclem  14443  hashfacen  14445  hashfacenOLD  14446  hashf1  14450  hashge2el2difr  14474  hashtpg  14478  ccatrn  14571  pfxsuffeqwrdeq  14680  wrd2ind  14705  scshwfzeqfzo  14809  wwlktovf1  14940  brtrclfv  14981  2shfti  15059  sqrtmsq2i  15366  limsupgle  15453  limsuple  15454  rlim  15471  clim0  15482  ello12  15492  elo12  15503  o1lo1  15513  rlimresb  15541  lo1add  15603  lo1mul  15604  rlimno1  15632  summo  15695  fsumsplit  15719  mertenslem2  15863  prodmo  15912  fprodsplit  15942  fprod2dlem  15956  cnso  16223  sqrt2irr  16225  dvdsval2  16233  alzdvds  16296  odd2np1lem  16316  even2n  16318  sumodd  16364  divalgb  16380  divalgmod  16382  bitsval  16398  bitsmod  16410  sadcp1  16429  gcddvds  16477  bezoutlem3  16516  bezout  16518  lcmfunsnlem2  16610  isprm3  16653  prmind2  16655  dvdsprime  16657  ge2nprmge4  16671  coprm  16681  prmdvdsexp  16685  prmdvdssqOLD  16689  crth  16746  pythagtriplem2  16785  pythagtrip  16802  pceu  16814  pc11  16848  vdwapval  16941  vdwapun  16942  vdwlem10  16958  vdwlem12  16960  vdwlem13  16961  ramval  16976  ramub1lem2  16995  prmlem0  17074  elrest  17408  imasleval  17522  ismri  17610  isacs  17630  isacs2  17632  acsfn1  17640  iscatd2  17660  homfeq  17673  catpropd  17688  ismon  17715  issect  17735  issect2  17736  isinv  17742  cic  17781  isssc  17802  isfunc  17849  funcres2b  17882  isnat  17936  fucinv  17964  iszeroo  17986  elhoma  18020  setcinv  18078  isprs  18288  isdrs  18292  lubeldm  18344  glbeldm  18357  istos  18409  tosso  18410  latnle  18464  latdisd  18488  isdlat  18513  isipodrs  18528  isacs5  18539  ismgmhm  18655  issubmgm  18661  ismhm  18741  issubm  18754  issubmndb  18756  sursubmefmnd  18847  injsubmefmnd  18848  grpsubeq0  18981  grpsubadd  18983  issubg  19080  subgmulg  19094  issubg3  19098  0subgOLD  19106  isnsg  19109  eqger  19132  eqglact  19133  eqgid  19134  cycsubmel  19154  isghm  19169  isga  19241  gacan  19255  gaorb  19257  gastacos  19260  orbsta  19263  elcntz  19272  elcntzsn  19275  sscntz  19276  gsmsymgreq  19386  psgnunilem5  19448  psgnunilem3  19450  psgneldm2  19458  psgneu  19460  psgnfitr  19471  dfod2  19518  isslw  19562  sylow2alem2  19572  lsmelvalx  19594  lsmcom2  19609  lsmass  19623  lssnle  19628  pj1eu  19650  lsmhash  19659  efgi  19673  efgval2  19678  efgtlen  19680  efgred  19702  lsmcomx  19810  iscyggen2  19835  iscyg3  19840  gsumval3eu  19858  gsumzsplit  19881  eldprd  19960  subgdmdprd  19990  dprddisj2  19995  dprd2da  19998  dmdprdsplit2lem  20001  dmdprdsplit2  20002  dprdsplit  20004  dmdprdpr  20005  pgpfac1lem3  20033  pgpfac1lem4  20034  pgpfac1lem5  20035  srgfcl  20135  dvdsr02  20310  isunit  20311  isirred  20357  isrnghmmul  20380  isrngim  20383  c0snmgmhm  20400  isrhm  20416  isrim0OLD  20419  isrim0  20421  isnzr2  20456  0ringnnzr  20461  subsubrng2  20500  subsubrg2  20537  issubrg3  20538  rngcinv  20569  ringcinv  20603  drngunit  20628  issdrg  20675  isabv  20698  islmod  20746  islss  20817  lspsnel  20886  islmhm  20911  lmhmeql  20939  islbs  20960  lsmspsn  20968  lsmelval2  20969  lspprel  20978  lvecvscan2  20999  lvecinv  21000  lspsneq  21009  lspsneu  21010  lspsolvlem  21029  islpidl  21214  lidldvgen  21223  isdomn3  21247  prmirredlem  21397  zrhrhmb  21435  zndvds  21482  elocv  21599  iscss  21614  pjdm  21640  ishil2  21652  isobs  21653  obslbs  21663  frlmelbas  21689  ellspd  21735  islinds  21742  islindf4  21771  aspval2  21830  mplsubglem  21940  mpllsslem  21941  mplmonmul  21973  opsrtoslem2  21999  ismhp  22064  mat1dimelbas  22372  dmatel  22394  scmatel  22406  mdetunilem8  22520  mdetunilem9  22521  maducoeval2  22541  cramer0  22591  cpmatel  22612  istop2g  22797  istopon  22813  toprntopon  22826  isbasis2g  22850  isbasis3g  22851  tgss2  22889  bastop1  22895  iscld  22930  elcls  22976  ntreq0  22980  isclo  22990  isclo2  22991  islp  23043  lpdifsn  23046  islpi  23052  restsn  23073  restlp  23086  ordtbaslem  23091  ordtbas2  23094  lmbr  23161  cnprest2  23193  ist0-3  23248  ist1-2  23250  cmpsublem  23302  cmpfi  23311  1stcrest  23356  2ndcdisj  23359  1stccnp  23365  llyi  23377  nllyi  23378  lly1stc  23399  iskgen3  23452  kgencn  23459  txbas  23470  eltx  23471  elpt  23475  xkoccn  23522  ptcnplem  23524  hausdiag  23548  hauseqlcld  23549  txlm  23551  txkgen  23555  kqfvima  23633  kqt0lem  23639  r0cld  23641  regr1lem2  23643  hmeoimaf1o  23673  isfbas2  23738  fbssfi  23740  trfbas2  23746  trfil2  23790  fmfnfmlem4  23860  elflim2  23867  flimrest  23886  cnflf  23905  txflf  23909  fclsopn  23917  ufilcmp  23935  cnfcf  23945  alexsubALTlem4  23953  cnextf  23969  tmdcn2  23992  qustgpopn  24023  qustgplem  24024  eltsms  24036  tsmsgsum  24042  tsmssplit  24055  elutop  24137  ustuqtop  24150  utopsnneiplem  24151  isusp  24165  isucn  24182  iscfilu  24192  ispsmet  24209  ismet  24228  isxmet  24229  metn0  24265  elblps  24292  elbl  24293  metrest  24432  metuel2  24473  psmetutop  24475  restmetu  24478  dscmet  24480  nrmmetd  24482  isngp3  24506  nmogelb  24632  isnmhm  24662  qtopbaslem  24674  xrsxmet  24724  icccmplem2  24738  metdseq0  24769  elcncf  24808  cnheibor  24880  ishtpy  24897  isphtpy  24906  isphtpc  24919  om1elbas  24958  elpi1  24971  isclmp  25023  nmhmcn  25046  iscph  25097  tcphcph  25164  lmmbrf  25189  iscfil  25192  iscfil2  25193  iscau  25203  caucfil  25210  iscmet  25211  iscmet3  25220  cfilucfil3  25247  bcthlem1  25251  rrxcph  25319  minveclem3b  25355  minveclem6  25361  evthicc2  25388  ovolfioo  25395  ovolficc  25396  ovolshftlem1  25437  ovolscalem1  25441  iundisj2  25477  dyadmbl  25528  volsup2  25533  mbfmax  25577  mbfsup  25592  mbfinf  25593  i1f1lem  25617  i1fres  25634  itg1climres  25643  itg2leub  25663  itg2seq  25671  itg2splitlem  25677  itg2monolem1  25679  itg2mono  25682  itg2cn  25692  iblpos  25721  iblcn  25727  itgsplit  25764  ellimc2  25805  dvreslem  25837  elcpn  25863  rolle  25921  dvlip  25925  dvivth  25942  tdeglem4  25994  tdeglem4OLD  25995  mdegleb  25999  deg1ldg  26027  ply1nzb  26057  ply1divmo  26070  ply1divex  26071  fta1glem2  26102  plyco0  26125  elply  26128  coeeu  26158  plydivex  26231  taylthlem2  26308  taylthlem2OLD  26309  radcnvlt1  26353  sincosq1sgn  26432  sincosq2sgn  26433  coseq1  26458  logreclem  26693  affineequiv  26754  affineequiv4  26757  dcubic  26777  quart  26792  atans2  26862  efrlim  26900  efrlimOLD  26901  mumullem2  27111  dvdsflsumcom  27119  fsumvma2  27146  chpchtsum  27151  chpub  27152  dchrelbas  27168  dchrelbas2  27169  dchreq  27190  dchrptlem2  27197  gausslemma2dlem0i  27296  lgsquadlem2  27313  m1lgs  27320  2lgsoddprmlem3  27346  2sqlem6  27355  2sqlem9  27359  2sqlem10  27360  2sq2  27365  2sqreunnltb  27393  2sqreuop  27394  2sqreuopnn  27395  2sqreuoplt  27396  2sqreuopltb  27397  2sqreuopnnlt  27398  2sqreuopnnltb  27399  2sqreuopb  27400  dchrisum0flb  27442  pntpbnd1  27518  pntlem3  27541  pntlemp  27542  sltval2  27588  sltintdifex  27593  sltres  27594  noextenddif  27600  nosepssdm  27618  nosupprefixmo  27632  noinfprefixmo  27633  nosupcbv  27634  nosupno  27635  nosupbnd1lem1  27640  noinfcbv  27649  noinfno  27650  noinfdm  27651  noinfres  27654  noinfbnd1lem1  27655  sletri3  27687  scutbdaylt  27750  sltrec  27752  elold  27795  ssltleft  27796  ssltright  27797  madebdayim  27813  madebdaylemlrcut  27824  madebday  27825  newbday  27827  sltlpss  27832  cofcutr  27843  cofcutrtime  27846  addsval2  27879  addsrid  27880  addsprop  27892  negsprop  27946  slt0neg2d  27962  subadds  27977  mulsval2lem  28009  mulsrid  28012  mulsprop  28029  mulscom  28038  mulsunif2  28069  mulscan2d  28078  precsexlemcbv  28103  precsexlem9  28112  recsex  28116  abssneg  28140  recut  28223  renegscl  28225  remulscl  28229  istrkg2ld  28263  iscgrg  28315  tgcgr4  28334  isismt  28337  tgellng  28356  tgcolg  28357  legov  28388  lnhl  28418  lmimid  28597  iscgra1  28613  ttgelitv  28692  elee  28704  mptelee  28705  colinearalglem2  28717  colinearalg  28720  ax5seglem5  28743  axeuclidlem  28772  axeuclid  28773  axcontlem1  28774  axcontlem2  28775  axcontlem5  28778  axcontlem7  28780  wrdupgr  28897  wrdumgr  28909  usgrexmpl  29075  uhgrspansubgrlem  29102  nbgrel  29152  nbupgrel  29157  nbgr2vtx1edg  29162  nbuhgr2vtx1edgblem  29163  nbuhgr2vtx1edgb  29164  nb3grprlem2  29193  nb3grpr2  29195  uvtx01vtx  29209  uvtxusgrel  29215  iscplgr  29227  vtxdun  29294  fusgrn0degnn0  29312  1loopgrnb0  29315  umgr2v2enb1  29339  vdiscusgrb  29343  wlkl1loop  29451  wlkv0  29464  wlklenvclwlk  29468  upgr2wlk  29481  wlkp1lem8  29493  upgrtrls  29514  upgristrl  29515  isspthonpth  29562  usgr2trlncl  29573  usgr2pthlem  29576  usgr2pth  29577  pthdlem1  29579  isclwlke  29590  isclwlkupgr  29591  uspgrn2crct  29618  wwlks  29645  iswwlksn  29648  wwlksnext  29703  wwlksnextinj  29709  wspn0  29734  wpthswwlks2on  29771  rusgrnumwwlkl1  29778  rusgrnumwwlkslem  29779  rusgrnumwwlkb0  29781  clwlkclwwlk  29811  clwwlknwwlksn  29847  clwwlkn2  29853  clwwlkel  29855  clwwlkwwlksb  29863  hashecclwwlkn1  29886  umgrhashecclwwlk  29887  clwwlknon1loop  29907  0wlk  29925  upgr3v3e3cycl  29989  upgr4cycl4dv4e  29994  dfconngr1  29997  vdn0conngrumgrv2  30005  eupth2lem2  30028  eupth2lem3lem6  30042  eucrct2eupth  30054  isfrgr  30069  frgr3v  30084  frgrncvvdeqlem3  30110  frgrncvvdeqlem6  30113  frgrwopreglem2  30122  fusgreg2wsplem  30142  2clwwlkel  30158  extwwlkfabel  30162  numclwwlk1lem2f1  30166  numclwwlk1lem2fo  30167  numclwwlk2lem1  30185  numclwlk2lem2f  30186  numclwlk2lem2f1o  30188  nrt2irr  30282  isgrpo  30306  isssp  30533  islno  30562  nmogtmnf  30579  nmoubi  30581  nmounbi  30585  isblo  30591  ishmo  30620  ubthlem1  30679  ubthlem2  30680  minvecolem5  30690  minvecolem6  30691  hvmulcan2  30882  hire  30903  ocel  31090  ocsh  31092  pjhthmo  31111  shscom  31128  shmodsi  31198  elspani  31352  adjsym  31642  eigorthi  31646  nmopgtmnf  31677  adjeu  31698  adjval2  31700  cnvadj  31701  nmopub  31717  nmfnleub  31734  eleigvec  31766  nmop0h  31800  largei  32076  mdbr2  32105  mddmd2  32118  mdsl2i  32131  chrelat3  32180  atnemeq0  32186  chirredlem1  32199  sumdmdii  32224  sumdmdlem  32227  dmdbr5ati  32231  cdjreui  32241  nelun  32308  disjabrex  32371  disjabrexf  32372  iundisj2f  32379  disjunsn  32383  brab2d  32396  br8d  32399  opabdm  32400  opabrn  32401  nfpconfp  32416  ofpreima  32450  funcnv5mpt  32453  suppiniseg  32466  1stpreima  32486  curry2ima  32488  f1od2  32503  fpwrelmap  32515  infxrge0gelb  32536  xnn01gt  32540  nndiffz1  32554  iundisj2fi  32565  tlt3  32697  toslublem  32699  tosglblem  32701  ismnt  32710  cntzun  32774  isarchi2  32893  erler  32979  qusker  33061  lsmsnorb  33100  lsmssass  33111  grplsm0l  33112  isprmidl  33154  ismxidl  33175  mxidlirred  33185  isrprm  33231  ply1degltel  33261  ply1degleel  33262  elirng  33360  algextdeglem8  33392  smatrcl  33397  zarcls  33475  rhmpreimacnlem  33485  cnvordtrestixx  33514  ordtconnlem1  33525  fsumcvg4  33551  lmdvg  33554  ind1a  33638  esum2dlem  33711  braew  33861  ismbfm  33870  mbfmcnt  33888  issibf  33953  eulerpartgbij  33992  eulerpartlemgvv  33996  eulerpartlemgh  33998  elorvc  34079  ballotlemfc0  34112  ballotlemfcc  34113  ballotlemodife  34117  sgn3da  34161  reprinrn  34250  reprdifc  34259  bnj1366  34460  bnj984  34583  bnj1171  34631  bnj1253  34648  bnj1417  34672  bnj1452  34683  lfuhgr3  34729  subfacp1lem3  34792  subfacp1lem5  34794  subfacp1lem6  34795  erdszelem9  34809  erdszelem10  34810  erdsze2lem2  34814  iscvm  34869  cvmlift2lem10  34922  snmlval  34941  satfv1  34973  satfvsucsuc  34975  satfrnmapom  34980  satf0op  34987  satf0n0  34988  sat1el2xp  34989  fmlafvel  34995  fmlaomn0  35000  gonarlem  35004  fmla0disjsuc  35008  fmlasucdisj  35009  satffunlem1lem1  35012  satffunlem2lem1  35014  satefvfmla0  35028  sategoelfvb  35029  mclsppslem  35193  climuzcnv  35275  br6  35351  elintfv  35360  dfdm5  35368  dfrn5  35369  dfon2lem7  35385  dfon2  35388  dfrdg2  35391  elfuns  35511  dfiota3  35519  brimg  35533  dfrdg4  35547  btwnouttr  35620  btwnexch  35621  funtransport  35627  cgr3permute1  35644  colinearperm1  35658  brsegle  35704  outsideoftr  35725  outsideofeu  35727  funray  35736  funline  35738  lineunray  35743  lineelsb2  35744  nn0prpwlem  35806  nn0prpw  35807  fneval  35836  topfneec  35839  filnetlem4  35865  ordcmp  35931  bj-sblem  36321  bj-sbceqgALT  36380  bj-elgab  36417  bj-clel3gALT  36527  bj-restpw  36571  bj-elid6  36649  bj-eldiag  36655  bj-eldiag2  36656  bj-imdirco  36669  f1omptsnlem  36815  mptsnunlem  36817  topdifinfeq  36829  isbasisrelowllem1  36834  isbasisrelowllem2  36835  relowlpssretop  36843  fvineqsnf1  36889  fvineqsneu  36890  wl-ifpimpr  36945  wl-sbcom2d  37028  wl-sbalnae  37029  curf  37071  unccur  37076  phpreu  37077  finixpnum  37078  ptrest  37092  poimirlem8  37101  poimirlem17  37110  poimirlem18  37111  poimirlem20  37113  poimirlem21  37114  poimirlem23  37116  poimirlem26  37119  poimirlem27  37120  poimirlem28  37121  poimirlem31  37124  poimirlem32  37125  poimir  37126  heicant  37128  mblfinlem1  37130  ismblfin  37134  mbfresfi  37139  itg2addnclem  37144  itg2addnclem2  37145  itg2addnc  37147  itg2gt0cn  37148  ftc1anclem6  37171  unirep  37187  indexa  37206  sdclem1  37216  fdc  37218  neificl  37226  istotbnd  37242  sstotbnd2  37247  isbnd  37253  isbnd3b  37258  heibor1lem  37282  heiborlem3  37286  rrnheibor  37310  ismgmOLD  37323  rngosn3  37397  isrngohom  37438  isrngoiso  37451  iscrngo2  37470  isidl  37487  ispridl  37507  pridlidl  37508  pridlnr  37509  pridl  37510  ismaxidl  37513  maxidlidl  37514  smprngopr  37525  prnc  37540  eldmres  37742  eldmressnALTV  37744  eldmqsres  37759  ideq2  37779  opideq  37815  cnvref5  37823  ecxrn  37859  disjressuc2  37860  disjecxrn  37861  disjecxrncnvep  37862  br2coss  37910  br1cossinres  37919  br1cossxrnres  37920  br1cossinidres  37921  br1cossincnvepres  37922  br1cossxrnidres  37923  br1cossxrncnvepres  37924  br1cosscnvxrn  37946  elrels5  37961  elrels6  37962  br1cossxrncnvssrres  37980  eldmqs1cossres  38131  erimeq2  38150  brabsb2  38334  prter3  38354  islshp  38451  islsat  38463  islshpat  38489  lcvexchlem1  38506  lsatnem0  38517  islfl  38532  ellkr  38561  lshpsmreu  38581  lshpkrlem3  38584  cvrval2  38746  cvrnbtwn2  38747  cvrnbtwn3  38748  isat  38758  leatb  38764  leat2  38766  cvlsupr2  38815  3dim0  38930  ps-2  38951  islln  38979  islln3  38983  llnexatN  38994  islpln  39003  islpln5  39008  lplnexatN  39036  islvol  39046  islvol5  39052  dalem-cly  39144  isline  39212  ispointN  39215  ispsubsp  39218  linepsubN  39225  elpmap  39231  isline4N  39250  elpadd  39272  paddcom  39286  pmapjoin  39325  pmapjat1  39326  llnexchb2  39342  elpclN  39365  pclcmpatN  39374  ispsubclN  39410  iswatN  39467  islhp  39469  islaut  39556  ispautN  39572  isldil  39583  isltrn  39592  isltrn2N  39593  isdilN  39627  istrnN  39630  cdlemefrs29bpre0  39869  cdleme40v  39942  istendo  40233  diaelval  40506  diaeldm  40509  dibopelvalN  40616  dibopelval2  40618  dib1dim  40638  dibglbN  40639  diblsmopel  40644  dicopelval  40650  dicelvalN  40651  dicelval3  40653  dicvalrelN  40658  diclspsn  40667  dihopelvalcpre  40721  xihopellsmN  40727  dihopellsm  40728  dih1  40759  dihglblem2aN  40766  dihglblem2N  40767  dihmeetlem4preN  40779  dihglb2  40815  dvh2dim  40918  islpolN  40956  lcfl7N  40974  lcdlss  41092  hdmap1fval  41269  hdmapfval  41300  hgmapfval  41359  hdmapglem7a  41400  hdmapoc  41404  lcmineqlem  41523  metakunt1  41657  sn-iotalem  41709  cxpi11d  41914  prjsperref  42030  isnacs  42124  mzpclval  42145  elmzpcl  42146  mzpcompact2lem  42171  eldiophb  42177  eldioph3  42186  fz1eqin  42189  diophrex  42195  eq0rabdioph  42196  rexrabdioph  42214  dvdsrabdioph  42230  eldioph4b  42231  eldioph4i  42232  elpell1qr  42267  elpell14qr  42269  elpell1234qr  42271  pell1234qrmulcl  42275  rmydioph  42435  rmxdioph  42437  aomclem8  42485  islmodfg  42493  islssfg2  42495  islnm2  42502  hbtlem2  42548  hbtlem5  42552  elmnc  42560  rngunsnply  42597  onsupmaxb  42667  orddif0suc  42697  onsucf1olem  42699  cantnf2  42754  tfsconcatb0  42773  tfsconcat0i  42774  tfsconcat00  42776  ofoafg  42783  oaun3lem1  42803  naddwordnexlem4  42831  fzunt  42885  fzuntd  42886  fzunt1d  42887  fzuntgd  42888  en2pr  42977  elmapintrab  43006  elinintrab  43007  brfvrcld  43121  brfvrcld2  43122  iunrelexpuztr  43149  brtrclfv2  43157  rfovcnvf1od  43434  fsovrfovd  43439  or3or  43453  ntrkbimka  43468  clsk3nimkb  43470  clsk1indlem4  43474  ntrclsiso  43497  ntrclskb  43499  ntrclsk3  43500  ntrclsk13  43501  ntrneiiso  43521  ntrneik2  43522  ntrneix2  43523  ntrneikb  43524  ntrneixb  43525  ntrneik3  43526  ntrneix3  43527  ntrneik13  43528  ntrneix13  43529  ntrneik4w  43530  gneispace3  43563  gneispace  43564  k0004lem1  43577  mnringmulrcld  43665  mnuunid  43714  grumnud  43723  expgrowth  43772  iotasbc2  43857  e2ebind  44002  fvelrnbf  44380  rnmptbdd  44621  rnmptbd2  44625  rnmptbd  44632  caucvgbf  44872  lmbr3v  45133  lmbr3  45135  xlimpnfxnegmnf  45202  xlimmnf  45229  xlimpnf  45230  xlimmnfmpt  45231  xlimpnfmpt  45232  dfxlim2  45236  xlimpnfxnegmnf2  45246  cncfshiftioo  45280  itgiccshift  45368  itgperiod  45369  stoweidlem31  45419  stoweidlem34  45422  stoweidlem59  45447  fourierdlem2  45497  fourierdlem3  45498  fourierdlem42  45537  fourierdlem54  45548  fourierdlem81  45575  fourierdlem87  45581  fourierdlem92  45586  fourierdlem105  45599  fourierdlem113  45607  fsetsniunop  46431  fcoresf1ob  46455  f1ocof1ob  46461  reuf1odnf  46487  euoreqb  46489  fnopafvb  46535  afvelrnb  46543  afvelrnb0  46544  dmafv2rnb  46609  dfatopafv2b  46626  fnopafv2b  46629  fun2dmnopgexmpl  46664  2ffzoeq  46708  iccpart  46756  iccpartgt  46767  fargshiftfo  46782  ichexmpl2  46810  sprvalpw  46820  sprsymrelfvlem  46830  paireqne  46851  prprvalpw  46855  prprelb  46856  prprelprb  46857  prprsprreu  46859  prprreueq  46860  fmtnoprmfac1lem  46904  requad2  46963  fpprel  47068  fppr2odd  47071  nnsum3primesgbe  47132  bgoldbtbndlem3  47147  bgoldbtbnd  47149  dfgric2  47181  isassintop  47272  assintopcllaw  47274  rngcinvALTV  47338  ringcinvALTV  47372  eliunxp2  47397  dmatALTbasel  47470  lcoval  47480  lco0  47495  lcoel0  47496  lindslinindsimp1  47525  lindslinindsimp2  47531  lincresunit3  47549  elbigo  47624  elbigo2  47625  nnolog2flm1  47663  rrx2pnedifcoorneor  47789  rrx2pnedifcoorneorr  47790  rrx2xpref1o  47791  rrx2line  47813  rrx2linest  47815  elrrx2linest2  47818  line2ylem  47824  line2x  47827  ralbidb  47872  ralbidc  47873  ipolub  47999  ipoglb  48002  catprsc  48019  catprsc2  48020  funcf2lem  48024  isthincd2lem2  48042  functhinc  48051  thincsect  48063