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  1030  19.17  2226  sb2ae  2500  sbcom3  2510  sbal1  2532  sbal2  2533  eqabrd  2877  cbvralf  3339  cbvreuwOLD  3394  cbvreu  3407  cbvrabwOLD  3453  cbvrab  3458  ceqsralt  3495  ralxpxfr2d  3625  clel2g  3638  clel4g  3642  elabd2  3649  ralab2  3680  rexab2  3682  reu7  3715  reu8  3716  2reu5  3741  ru  3763  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  ralss  4033  ralssOLD  4035  rexssOLD  4036  sbcssg  4495  rabsneq  4620  elpwunsn  4660  reuprg0  4678  reuprg  4679  prssg  4795  ssunsn2  4803  eqsn  4805  prneimg2  4831  preqsnd  4835  2ralunsn  4871  eluniab  4897  csbuni  4912  elintabg  4933  elintabOLD  4935  dfiun2gOLD  5007  dfiin2g  5008  disjprg  5115  disjxun  5117  cbvopab1g  5194  cbvmptf  5221  cbvmptfg  5222  al0ssb  5278  reusv3  5375  elopg  5441  opthneg  5456  opeqsng  5478  sotrieq2  5593  frsn  5742  eliunxp  5817  exopxfr2  5824  relop  5830  eldm2g  5879  reldm0  5907  relrn0  5952  restidsing  6040  elimasng  6076  asymref2  6106  somin1  6122  imadifssran  6140  xpnz  6148  xpcan  6165  xpcan2  6166  relsn2  6201  dfpo2  6285  ordtri2  6387  ordtri3  6388  oneqmini  6405  cbviota  6492  iotaval2  6498  iotavalOLD  6504  iota1  6507  sniota  6521  fncnv  6608  fnres  6664  sbcfng  6702  sbcfg  6703  brprcneu  6865  brprcneuALT  6866  fnopfvb  6929  fvelrnb  6938  funimass4  6942  unima  6953  dffv2  6973  fvopab3g  6980  eqfnfv  7020  eqfnfv3  7022  eqfnfv2f  7024  fvreseq0  7027  fnreseql  7037  fniniseg  7049  respreima  7055  rexrn  7076  ralrn  7077  f1ompt  7100  fssrescdmd  7115  fsn  7124  funopsn  7137  funsndifnop  7140  fprb  7185  tpres  7192  eufnfv  7220  ralima  7228  reximaOLD  7230  ralimaOLD  7231  dff13  7246  f13dfv  7266  fliftfun  7304  isocnv  7322  isoini  7330  f1oiso  7343  fnssintima  7354  imaeqsexvOLD  7355  cbvriota  7373  riotaeqimp  7386  eusvobj2  7395  oprabidw  7434  oprabid  7435  f1opr  7461  eloprabga  7514  resoprab  7523  eqfnov  7534  eqfnov2  7535  ov6g  7569  ovelrn  7581  funimassov  7582  ovelimab  7583  ndmovg  7588  caovord2  7617  imaeqexov  7643  imaeqalov  7644  tfisi  7852  eqop  8028  releldm2  8040  dfoprab4  8052  opiota  8056  bropopvvv  8087  bropfvvvv  8089  fparlem1  8109  fparlem2  8110  xporderlem  8124  poxp  8125  soxp  8126  fnwelem  8128  xpord2lem  8139  poxp2  8140  frxp2  8141  xpord2indlem  8144  poxp3  8147  frxp3  8148  xpord3pred  8149  xpord3inddlem  8151  elsuppfng  8166  elsuppfn  8167  rexsupp  8179  suppcoss  8204  mpoxopovel  8217  brtpos2  8229  brtpos0  8230  rntpos  8236  dftpos3  8241  tpostpos  8243  tpossym  8255  tposoprab  8259  mpocurryd  8266  frrlem1  8283  wfrlem1OLD  8320  oevn0  8525  om00el  8586  omordlim  8587  omlimcl  8588  oeoa  8607  oeoe  8609  oeeulem  8611  oeeui  8612  oaabs2  8659  omabs  8661  cofonr  8684  naddunif  8703  naddasslem1  8704  naddasslem2  8705  erth2  8769  qliftfun  8814  erovlem  8825  ecopovsym  8831  mapdm0  8854  elpmg  8855  elpm2g  8856  dom2lem  9004  mapsnend  9048  xpdom2  9079  omxpenlem  9085  0sdomg  9116  0sdomgOLD  9117  fodomr  9140  xpf1o  9151  mapen  9153  ac6sfi  9290  fodomfir  9338  mapfien  9418  marypha2lem3  9447  ordtypelem7  9536  wemaplem1  9558  wemapsolem  9562  elharval  9573  brwdom3  9594  unwdomg  9596  xpwdomg  9597  inf3lem1  9640  cantnfs  9678  cantnfp1lem2  9691  cantnflem1d  9700  cantnflem1  9701  wemapwe  9709  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  r1sdom  9786  rankr1ai  9810  rankval2  9830  unbndrank  9854  rankunb  9862  tcrank  9896  bnd2  9905  cardnueq0  9976  iscard2  9988  r0weon  10024  fseqenlem1  10036  alephord2  10088  cardaleph  10101  aceq0  10130  dfac5lem4OLD  10140  dfac5  10141  kmlem14  10176  cfsmolem  10282  isfin4-2  10326  fin23lem26  10337  fin23lem22  10339  fin1a2lem7  10418  axdc3lem2  10463  axdc3  10466  zfac  10472  zornn0g  10517  axdclem  10531  brdom3  10540  zfcndac  10631  fpwwe2lem7  10649  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  pwfseqlem3  10672  winainflem  10705  eltsk2g  10763  inatsk  10790  axgroth2  10837  axgroth6  10840  sstskm  10854  ltexpi  10914  ordpinq  10955  lterpq  10982  ltanq  10983  ltmnq  10984  genpv  11011  genpelv  11012  prlem934  11045  prlem936  11059  addcmpblnr  11081  ltsrpr  11089  ltsosr  11106  mulgt0sr  11117  supsrlem  11123  elreal2  11144  ltresr  11152  ltresr2  11153  axrrecex  11175  axpre-ltadd  11179  axpre-mulgt0  11180  axpre-sup  11181  subcan2  11506  negcon1  11533  negcon2  11534  lt0neg1  11741  lt0neg2  11742  le0neg1  11743  le0neg2  11744  msq0d  11884  mulcan2g  11889  divmul2  11898  reclt1  12135  recgt1  12136  infm3  12199  suprlub  12204  suprleub  12206  infregelb  12224  addltmul  12475  arch  12496  elznn0  12601  nn0lt2  12654  eluz1  12854  raluz  12910  rexuz  12912  nnwof  12928  cnref1o  12999  ltxr  13129  xrltlen  13160  dflt2  13162  xrrebnd  13182  xlt0neg1  13233  xlt0neg2  13234  xle0neg1  13235  xle0neg2  13236  xmulneg1  13283  supxrbnd  13342  elixx1  13369  ixxun  13376  elioo2  13401  elicc4  13428  elioopnf  13458  elioomnf  13459  iccneg  13487  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  iccf1o  13511  elfz1  13527  0fz1  13559  elfzp1  13589  fzpr  13594  uzsplit  13611  elfzm1b  13617  elfzp12  13618  fznn0  13634  fvinim0ffz  13800  injresinj  13802  fleqceilz  13869  zmodid2  13914  fsuppmapnn0fiub0  14009  bernneq  14245  hasheqf1o  14365  euhash1  14436  hashbclem  14468  hashfacen  14470  hashf1  14473  hashge2el2difr  14497  hashtpg  14501  ccatrn  14605  pfxsuffeqwrdeq  14714  wrd2ind  14739  scshwfzeqfzo  14843  wwlktovf1  14974  brtrclfv  15019  2shfti  15097  sqrtmsq2i  15404  limsupgle  15491  limsuple  15492  rlim  15509  clim0  15520  ello12  15530  elo12  15541  o1lo1  15551  rlimresb  15579  lo1add  15641  lo1mul  15642  rlimno1  15668  summo  15731  fsumsplit  15755  mertenslem2  15899  prodmo  15950  fprodsplit  15980  fprod2dlem  15994  cnso  16263  sqrt2irr  16265  dvdsval2  16273  alzdvds  16337  odd2np1lem  16357  even2n  16359  sumodd  16405  divalgb  16421  divalgmod  16423  bitsval  16441  bitsmod  16453  sadcp1  16472  gcddvds  16520  bezoutlem3  16558  bezout  16560  lcmfunsnlem2  16657  isprm3  16700  prmind2  16702  dvdsprime  16704  ge2nprmge4  16718  coprm  16728  prmdvdsexp  16732  crth  16795  pythagtriplem2  16835  pythagtrip  16852  pceu  16864  pc11  16898  vdwapval  16991  vdwapun  16992  vdwlem10  17008  vdwlem12  17010  vdwlem13  17011  ramval  17026  ramub1lem2  17045  prmlem0  17123  elrest  17439  imasleval  17553  ismri  17641  isacs  17661  isacs2  17663  acsfn1  17671  iscatd2  17691  homfeq  17704  catpropd  17719  ismon  17744  issect  17764  issect2  17765  isinv  17771  cic  17810  isssc  17831  isfunc  17875  funcres2b  17908  isnat  17961  fucinv  17987  iszeroo  18009  elhoma  18043  setcinv  18101  isprs  18306  isdrs  18311  lubeldm  18361  glbeldm  18374  istos  18426  tosso  18427  latnle  18481  latdisd  18505  isdlat  18530  isipodrs  18545  isacs5  18556  ismgmhm  18672  issubmgm  18678  ismhm  18761  issubm  18779  issubmndb  18781  sursubmefmnd  18872  injsubmefmnd  18873  grpsubeq0  19007  grpsubadd  19009  issubg  19107  subgmulg  19121  issubg3  19125  0subgOLD  19133  isnsg  19136  eqger  19159  eqglact  19160  eqgid  19161  cycsubmel  19181  isghm  19196  isghmOLD  19197  isga  19272  gacan  19286  gaorb  19288  gastacos  19291  orbsta  19294  elcntz  19303  elcntzsn  19306  sscntz  19307  gsmsymgreq  19411  psgnunilem5  19473  psgnunilem3  19475  psgneldm2  19483  psgneu  19485  psgnfitr  19496  dfod2  19543  isslw  19587  sylow2alem2  19597  lsmelvalx  19619  lsmcom2  19634  lsmass  19648  lssnle  19653  pj1eu  19675  lsmhash  19684  efgi  19698  efgval2  19703  efgtlen  19705  efgred  19727  lsmcomx  19835  iscyggen2  19860  iscyg3  19865  gsumval3eu  19883  gsumzsplit  19906  eldprd  19985  subgdmdprd  20015  dprddisj2  20020  dprd2da  20023  dmdprdsplit2lem  20026  dmdprdsplit2  20027  dprdsplit  20029  dmdprdpr  20030  pgpfac1lem3  20058  pgpfac1lem4  20059  pgpfac1lem5  20060  srgfcl  20154  dvdsr02  20330  isunit  20331  isirred  20377  isrnghmmul  20400  isrngim  20403  c0snmgmhm  20420  isrhm  20436  isrim0OLD  20439  isrim0  20441  isnzr2  20476  0ringnnzr  20483  subsubrng2  20522  subsubrg2  20557  issubrg3  20558  rngcinv  20595  ringcinv  20629  isdomn3  20673  drngunit  20692  issdrg  20746  isabv  20769  islmod  20819  islss  20889  ellspsn  20958  islmhm  20983  lmhmeql  21011  islbs  21032  lsmspsn  21040  lsmelval2  21041  lspprel  21050  lvecvscan2  21071  lvecinv  21072  lspsneq  21081  lspsneu  21082  lspsolvlem  21101  islpidl  21284  lidldvgen  21293  prmirredlem  21431  zrhrhmb  21469  zndvds  21508  elocv  21626  iscss  21641  pjdm  21665  ishil2  21677  isobs  21678  obslbs  21688  frlmelbas  21714  ellspd  21760  islinds  21767  islindf4  21796  aspval2  21856  mplsubglem  21957  mpllsslem  21958  mplmonmul  21992  opsrtoslem2  22012  ismhp  22076  mat1dimelbas  22407  dmatel  22429  scmatel  22441  mdetunilem8  22555  mdetunilem9  22556  maducoeval2  22576  cramer0  22626  cpmatel  22647  istop2g  22832  istopon  22848  toprntopon  22861  isbasis2g  22884  isbasis3g  22885  tgss2  22923  bastop1  22929  iscld  22963  elcls  23009  ntreq0  23013  isclo  23023  isclo2  23024  islp  23076  lpdifsn  23079  islpi  23085  restsn  23106  restlp  23119  ordtbaslem  23124  ordtbas2  23127  lmbr  23194  cnprest2  23226  ist0-3  23281  ist1-2  23283  cmpsublem  23335  cmpfi  23344  1stcrest  23389  2ndcdisj  23392  1stccnp  23398  llyi  23410  nllyi  23411  lly1stc  23432  iskgen3  23485  kgencn  23492  txbas  23503  eltx  23504  elpt  23508  xkoccn  23555  ptcnplem  23557  hausdiag  23581  hauseqlcld  23582  txlm  23584  txkgen  23588  kqfvima  23666  kqt0lem  23672  r0cld  23674  regr1lem2  23676  hmeoimaf1o  23706  isfbas2  23771  fbssfi  23773  trfbas2  23779  trfil2  23823  fmfnfmlem4  23893  elflim2  23900  flimrest  23919  cnflf  23938  txflf  23942  fclsopn  23950  ufilcmp  23968  cnfcf  23978  alexsubALTlem4  23986  cnextf  24002  tmdcn2  24025  qustgpopn  24056  qustgplem  24057  eltsms  24069  tsmsgsum  24075  tsmssplit  24088  elutop  24170  ustuqtop  24183  utopsnneiplem  24184  isusp  24198  isucn  24214  iscfilu  24224  ispsmet  24241  ismet  24260  isxmet  24261  metn0  24297  elblps  24324  elbl  24325  metrest  24461  metuel2  24502  psmetutop  24504  restmetu  24507  dscmet  24509  nrmmetd  24511  isngp3  24535  nmogelb  24653  isnmhm  24683  qtopbaslem  24695  xrsxmet  24747  icccmplem2  24761  metdseq0  24792  elcncf  24831  cnheibor  24903  ishtpy  24920  isphtpy  24929  isphtpc  24942  om1elbas  24981  elpi1  24994  isclmp  25046  nmhmcn  25069  iscph  25120  tcphcph  25187  lmmbrf  25212  iscfil  25215  iscfil2  25216  iscau  25226  caucfil  25233  iscmet  25234  iscmet3  25243  cfilucfil3  25270  bcthlem1  25274  rrxcph  25342  minveclem3b  25378  minveclem6  25384  evthicc2  25411  ovolfioo  25418  ovolficc  25419  ovolshftlem1  25460  ovolscalem1  25464  iundisj2  25500  dyadmbl  25551  volsup2  25556  mbfmax  25600  mbfsup  25615  mbfinf  25616  i1f1lem  25640  i1fres  25656  itg1climres  25665  itg2leub  25685  itg2seq  25693  itg2splitlem  25699  itg2monolem1  25701  itg2mono  25704  itg2cn  25714  iblpos  25744  iblcn  25750  itgsplit  25787  ellimc2  25828  dvreslem  25860  elcpn  25886  rolle  25944  dvlip  25948  dvivth  25965  tdeglem4  26015  mdegleb  26019  deg1ldg  26047  ply1nzb  26078  ply1divmo  26091  ply1divex  26092  fta1glem2  26124  plyco0  26147  elply  26150  coeeu  26180  plydivex  26255  taylthlem2  26332  taylthlem2OLD  26333  radcnvlt1  26377  sincosq1sgn  26457  sincosq2sgn  26458  coseq1  26484  logreclem  26722  affineequiv  26783  affineequiv4  26786  dcubic  26806  quart  26821  atans2  26891  efrlim  26929  efrlimOLD  26930  mumullem2  27140  dvdsflsumcom  27148  fsumvma2  27175  chpchtsum  27180  chpub  27181  dchrelbas  27197  dchrelbas2  27198  dchreq  27219  dchrptlem2  27226  gausslemma2dlem0i  27325  lgsquadlem2  27342  m1lgs  27349  2lgsoddprmlem3  27375  2sqlem6  27384  2sqlem9  27388  2sqlem10  27389  2sq2  27394  2sqreunnltb  27422  2sqreuop  27423  2sqreuopnn  27424  2sqreuoplt  27425  2sqreuopltb  27426  2sqreuopnnlt  27427  2sqreuopnnltb  27428  2sqreuopb  27429  dchrisum0flb  27471  pntpbnd1  27547  pntlem3  27570  pntlemp  27571  sltval2  27618  sltintdifex  27623  sltres  27624  noextenddif  27630  nosepssdm  27648  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupno  27665  nosupbnd1lem1  27670  noinfcbv  27679  noinfno  27680  noinfdm  27681  noinfres  27684  noinfbnd1lem1  27685  sletri3  27717  scutbdaylt  27780  sltrec  27782  elold  27825  ssltleft  27826  ssltright  27827  madebdayim  27843  madebdaylemlrcut  27854  madebday  27855  newbday  27857  sltlpss  27862  cofcutr  27875  cofcutrtime  27878  addsval2  27913  addsrid  27914  addsprop  27926  negsprop  27984  slt0neg2d  28000  subadds  28017  mulsval2lem  28053  mulsrid  28056  mulsprop  28073  mulscom  28082  mulsunif2  28113  mulscan2d  28122  precsexlemcbv  28147  precsexlem9  28156  recsex  28160  abssneg  28188  dfnns2  28279  elnnzs  28304  elznns  28305  n0seo  28322  zs12bday  28341  recut  28345  renegscl  28347  remulscl  28351  istrkg2ld  28385  iscgrg  28437  tgcgr4  28456  isismt  28459  tgellng  28478  tgcolg  28479  legov  28510  lnhl  28540  lmimid  28719  iscgra1  28735  ttgelitv  28808  elee  28819  mptelee  28820  colinearalglem2  28832  colinearalg  28835  ax5seglem5  28858  axeuclidlem  28887  axeuclid  28888  axcontlem1  28889  axcontlem2  28890  axcontlem5  28893  axcontlem7  28895  wrdupgr  29010  wrdumgr  29022  uhgrspansubgrlem  29215  nbgrel  29265  nbupgrel  29270  nbgr2vtx1edg  29275  nbuhgr2vtx1edgblem  29276  nbuhgr2vtx1edgb  29277  nb3grprlem2  29306  nb3grpr2  29308  uvtx01vtx  29322  uvtxusgrel  29328  iscplgr  29340  vtxdun  29407  fusgrn0degnn0  29425  1loopgrnb0  29428  umgr2v2enb1  29452  vdiscusgrb  29456  wlkl1loop  29564  wlkv0  29577  wlklenvclwlk  29581  upgr2wlk  29594  wlkp1lem8  29606  upgrtrls  29627  upgristrl  29628  dfpth2  29657  isspthonpth  29677  usgr2trlncl  29688  usgr2pthlem  29691  usgr2pth  29692  pthdlem1  29694  isclwlke  29705  isclwlkupgr  29706  uspgrn2crct  29736  wwlks  29763  iswwlksn  29766  wwlksnext  29821  wwlksnextinj  29827  wspn0  29852  wpthswwlks2on  29889  rusgrnumwwlkl1  29896  rusgrnumwwlkslem  29897  rusgrnumwwlkb0  29899  clwlkclwwlk  29929  clwwlknwwlksn  29965  clwwlkn2  29971  clwwlkel  29973  clwwlkwwlksb  29981  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwwlknon1loop  30025  0wlk  30043  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  dfconngr1  30115  vdn0conngrumgrv2  30123  eupth2lem2  30146  eupth2lem3lem6  30160  eucrct2eupth  30172  isfrgr  30187  frgr3v  30202  frgrncvvdeqlem3  30228  frgrncvvdeqlem6  30231  frgrwopreglem2  30240  fusgreg2wsplem  30260  2clwwlkel  30276  extwwlkfabel  30280  numclwwlk1lem2f1  30284  numclwwlk1lem2fo  30285  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  nrt2irr  30400  isgrpo  30424  isssp  30651  islno  30680  nmogtmnf  30697  nmoubi  30699  nmounbi  30703  isblo  30709  ishmo  30738  ubthlem1  30797  ubthlem2  30798  minvecolem5  30808  minvecolem6  30809  hvmulcan2  31000  hire  31021  ocel  31208  ocsh  31210  pjhthmo  31229  shscom  31246  shmodsi  31316  elspani  31470  adjsym  31760  eigorthi  31764  nmopgtmnf  31795  adjeu  31816  adjval2  31818  cnvadj  31819  nmopub  31835  nmfnleub  31852  eleigvec  31884  nmop0h  31918  largei  32194  mdbr2  32223  mddmd2  32236  mdsl2i  32249  chrelat3  32298  atnemeq0  32304  chirredlem1  32317  sumdmdii  32342  sumdmdlem  32345  dmdbr5ati  32349  cdjreui  32359  nelun  32440  tpssg  32464  disjabrex  32509  disjabrexf  32510  iundisj2f  32517  disjunsn  32521  brab2d  32533  br8d  32536  opabdm  32537  opabrn  32538  nfpconfp  32556  ofpreima  32589  funcnv5mpt  32592  suppiniseg  32609  1stpreima  32630  curry2ima  32632  f1od2  32644  fpwrelmap  32656  infxrge0gelb  32689  xnn01gt  32693  nndiffz1  32709  iundisj2fi  32720  fzo0opth  32728  sgn3da  32759  ind1a  32782  tlt3  32896  toslublem  32898  tosglblem  32900  ismnt  32909  cntzun  33008  isarchi2  33129  erler  33206  qusker  33310  unitprodclb  33350  lsmsnorb  33352  lsmssass  33363  grplsm0l  33364  isprmidl  33399  ismxidl  33423  mxidlirred  33433  isrprm  33478  ufdprmidl  33502  1arithufdlem4  33508  ply1degltel  33550  ply1degleel  33551  elirng  33673  algextdeglem8  33704  fldext2chn  33708  constrextdg2  33729  constrfiss  33731  smatrcl  33773  zarcls  33851  rhmpreimacnlem  33861  cnvordtrestixx  33890  ordtconnlem1  33901  fsumcvg4  33927  lmdvg  33930  esum2dlem  34069  braew  34219  ismbfm  34228  mbfmcnt  34246  issibf  34311  eulerpartgbij  34350  eulerpartlemgvv  34354  eulerpartlemgh  34356  elorvc  34438  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemodife  34476  reprinrn  34596  reprdifc  34605  bnj1366  34806  bnj984  34929  bnj1171  34977  bnj1253  34994  bnj1417  35018  bnj1452  35029  lfuhgr3  35088  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  erdszelem9  35167  erdszelem10  35168  erdsze2lem2  35172  iscvm  35227  cvmlift2lem10  35280  snmlval  35299  satfv1  35331  satfvsucsuc  35333  satfrnmapom  35338  satf0op  35345  satf0n0  35346  sat1el2xp  35347  fmlafvel  35353  fmlaomn0  35358  gonarlem  35362  fmla0disjsuc  35366  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  satefvfmla0  35386  sategoelfvb  35387  mclsppslem  35551  r1peuqusdeg1  35611  climuzcnv  35639  br6  35720  elintfv  35728  dfdm5  35736  dfrn5  35737  dfon2lem7  35753  dfon2  35756  dfrdg2  35759  elfuns  35879  dfiota3  35887  brimg  35901  dfrdg4  35915  btwnouttr  35988  btwnexch  35989  funtransport  35995  cgr3permute1  36012  colinearperm1  36026  brsegle  36072  outsideoftr  36093  outsideofeu  36095  funray  36104  funline  36106  lineunray  36111  lineelsb2  36112  nn0prpwlem  36286  nn0prpw  36287  fneval  36316  topfneec  36319  filnetlem4  36345  ordcmp  36411  bj-sblem  36808  bj-sbceqgALT  36866  bj-elgab  36903  bj-clel3gALT  37012  bj-restpw  37056  bj-elid6  37134  bj-eldiag  37140  bj-eldiag2  37141  bj-imdirco  37154  f1omptsnlem  37300  mptsnunlem  37302  topdifinfeq  37314  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlpssretop  37328  fvineqsnf1  37374  fvineqsneu  37375  wl-ifpimpr  37430  wl-sbcom2d  37525  wl-sbalnae  37526  curf  37568  unccur  37573  phpreu  37574  finixpnum  37575  ptrest  37589  poimirlem8  37598  poimirlem17  37607  poimirlem18  37608  poimirlem20  37610  poimirlem21  37611  poimirlem23  37613  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem31  37621  poimirlem32  37622  poimir  37623  heicant  37625  mblfinlem1  37627  ismblfin  37631  mbfresfi  37636  itg2addnclem  37641  itg2addnclem2  37642  itg2addnc  37644  itg2gt0cn  37645  ftc1anclem6  37668  unirep  37684  indexa  37703  sdclem1  37713  fdc  37715  neificl  37723  istotbnd  37739  sstotbnd2  37744  isbnd  37750  isbnd3b  37755  heibor1lem  37779  heiborlem3  37783  rrnheibor  37807  ismgmOLD  37820  rngosn3  37894  isrngohom  37935  isrngoiso  37948  iscrngo2  37967  isidl  37984  ispridl  38004  pridlidl  38005  pridlnr  38006  pridl  38007  ismaxidl  38010  maxidlidl  38011  smprngopr  38022  prnc  38037  eldmres  38234  eldmressnALTV  38236  eldmqsres  38251  ideq2  38271  opideq  38307  cnvref5  38315  ecxrn  38351  disjressuc2  38352  disjecxrn  38353  disjecxrncnvep  38354  br2coss  38402  br1cossinres  38411  br1cossxrnres  38412  br1cossinidres  38413  br1cossincnvepres  38414  br1cossxrnidres  38415  br1cossxrncnvepres  38416  br1cosscnvxrn  38438  elrels5  38453  elrels6  38454  br1cossxrncnvssrres  38472  eldmqs1cossres  38623  erimeq2  38642  brabsb2  38826  prter3  38846  islshp  38943  islsat  38955  islshpat  38981  lcvexchlem1  38998  lsatnem0  39009  islfl  39024  ellkr  39053  lshpsmreu  39073  lshpkrlem3  39076  cvrval2  39238  cvrnbtwn2  39239  cvrnbtwn3  39240  isat  39250  leatb  39256  leat2  39258  cvlsupr2  39307  3dim0  39422  ps-2  39443  islln  39471  islln3  39475  llnexatN  39486  islpln  39495  islpln5  39500  lplnexatN  39528  islvol  39538  islvol5  39544  dalem-cly  39636  isline  39704  ispointN  39707  ispsubsp  39710  linepsubN  39717  elpmap  39723  isline4N  39742  elpadd  39764  paddcom  39778  pmapjoin  39817  pmapjat1  39818  llnexchb2  39834  elpclN  39857  pclcmpatN  39866  ispsubclN  39902  iswatN  39959  islhp  39961  islaut  40048  ispautN  40064  isldil  40075  isltrn  40084  isltrn2N  40085  isdilN  40119  istrnN  40122  cdlemefrs29bpre0  40361  cdleme40v  40434  istendo  40725  diaelval  40998  diaeldm  41001  dibopelvalN  41108  dibopelval2  41110  dib1dim  41130  dibglbN  41131  diblsmopel  41136  dicopelval  41142  dicelvalN  41143  dicelval3  41145  dicvalrelN  41150  diclspsn  41159  dihopelvalcpre  41213  xihopellsmN  41219  dihopellsm  41220  dih1  41251  dihglblem2aN  41258  dihglblem2N  41259  dihmeetlem4preN  41271  dihglb2  41307  dvh2dim  41410  islpolN  41448  lcfl7N  41466  lcdlss  41584  hdmap1fval  41761  hdmapfval  41792  hgmapfval  41851  hdmapglem7a  41892  hdmapoc  41896  lcmineqlem  42011  metakunt1  42164  sn-iotalem  42218  cxpi11d  42339  fimgmcyclem  42503  fimgmcyc  42504  prjsperref  42576  isnacs  42674  mzpclval  42695  elmzpcl  42696  mzpcompact2lem  42721  eldiophb  42727  eldioph3  42736  fz1eqin  42739  diophrex  42745  eq0rabdioph  42746  rexrabdioph  42764  dvdsrabdioph  42780  eldioph4b  42781  eldioph4i  42782  elpell1qr  42817  elpell14qr  42819  elpell1234qr  42821  pell1234qrmulcl  42825  rmydioph  42985  rmxdioph  42987  aomclem8  43032  islmodfg  43040  islssfg2  43042  islnm2  43049  hbtlem2  43095  hbtlem5  43099  elmnc  43107  rngunsnply  43140  onsupmaxb  43210  orddif0suc  43239  onsucf1olem  43241  cantnf2  43296  tfsconcatb0  43315  tfsconcat0i  43316  tfsconcat00  43318  ofoafg  43325  oaun3lem1  43345  naddwordnexlem4  43372  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  en2pr  43518  elmapintrab  43547  elinintrab  43548  brfvrcld  43662  brfvrcld2  43663  iunrelexpuztr  43690  brtrclfv2  43698  rfovcnvf1od  43975  fsovrfovd  43980  or3or  43994  ntrkbimka  44009  clsk3nimkb  44011  clsk1indlem4  44015  ntrclsiso  44038  ntrclskb  44040  ntrclsk3  44041  ntrclsk13  44042  ntrneiiso  44062  ntrneik2  44063  ntrneix2  44064  ntrneikb  44065  ntrneixb  44066  ntrneik3  44067  ntrneix3  44068  ntrneik13  44069  ntrneix13  44070  ntrneik4w  44071  gneispace3  44104  gneispace  44105  k0004lem1  44118  mnringmulrcld  44200  mnuunid  44249  grumnud  44258  expgrowth  44307  iotasbc2  44392  e2ebind  44536  modelaxreplem3  44953  modelac8prim  44965  permaxrep  44979  fvelrnbf  44990  rnmptbdd  45217  rnmptbd2  45221  rnmptbd  45228  caucvgbf  45464  lmbr3v  45722  lmbr3  45724  xlimpnfxnegmnf  45791  xlimmnf  45818  xlimpnf  45819  xlimmnfmpt  45820  xlimpnfmpt  45821  dfxlim2  45825  xlimpnfxnegmnf2  45835  cncfshiftioo  45869  itgiccshift  45957  itgperiod  45958  stoweidlem31  46008  stoweidlem34  46011  stoweidlem59  46036  fourierdlem2  46086  fourierdlem3  46087  fourierdlem42  46126  fourierdlem54  46137  fourierdlem81  46164  fourierdlem87  46170  fourierdlem92  46175  fourierdlem105  46188  fourierdlem113  46196  fsetsniunop  47026  fcoresf1ob  47050  f1ocof1ob  47058  reuf1odnf  47084  euoreqb  47086  fnopafvb  47132  afvelrnb  47140  afvelrnb0  47141  dmafv2rnb  47206  dfatopafv2b  47223  fnopafv2b  47226  fun2dmnopgexmpl  47261  2ffzoeq  47304  addmodne  47321  iccpart  47378  iccpartgt  47389  fargshiftfo  47404  ichexmpl2  47432  sprvalpw  47442  sprsymrelfvlem  47452  paireqne  47473  prprvalpw  47477  prprelb  47478  prprelprb  47479  prprsprreu  47481  prprreueq  47482  fmtnoprmfac1lem  47526  requad2  47585  fpprel  47690  fppr2odd  47693  nnsum3primesgbe  47754  bgoldbtbndlem3  47769  bgoldbtbnd  47771  vopnbgrel  47815  upgrimpths  47870  dfgric2  47876  grtriprop  47901  isgrtri  47903  stgredgel  47917  gpgvtxel  47999  gpgvtxedg1  48016  isassintop  48133  assintopcllaw  48135  rngcinvALTV  48199  ringcinvALTV  48233  eliunxp2  48257  dmatALTbasel  48326  lcoval  48336  lco0  48351  lcoel0  48352  lindslinindsimp1  48381  lindslinindsimp2  48387  lincresunit3  48405  elbigo  48479  elbigo2  48480  nnolog2flm1  48518  rrx2pnedifcoorneor  48644  rrx2pnedifcoorneorr  48645  rrx2xpref1o  48646  rrx2line  48668  rrx2linest  48670  elrrx2linest2  48673  line2ylem  48679  line2x  48682  ralbidb  48727  ralbidc  48728  brab2dd  48754  resinsnALT  48796  ipolub  48910  ipoglb  48913  catprsc  48936  catprsc2  48937  funcf2lem  48994  0funcglem  48996  0funcg2  48997  0funclem  48999  termopropd  49109  fucofulem2  49170  isthincd2lem2  49269  functhinc  49282  thincsect  49301  2arwcatlem1  49420  setc1onsubc  49427