Theorem bitrdi 288

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 280	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bitr2di  289  bitr4di  290  3bitr3g  314  bibi2i  338  ibibr  369  biancomd  464  pm5.75  1036  19.17  2238  sb2ae  2504  sbcom3  2514  sbal1  2536  sbal2  2537  eqabrd  2881  cbvralf  3325  cbvreu  3384  cbvrabwOLD  3428  cbvrab  3431  ceqsralt  3467  ralxpxfr2d  3591  clel2g  3604  clel4g  3608  elabd2  3615  ralab2  3645  rexab2  3647  reu7  3680  reu8  3681  2reu5  3706  ru  3728  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  ralss  3994  ralssOLD  3996  rexssOLD  3997  sbcssg  4456  rabsneq  4581  elpwunsn  4623  reuprg0  4641  reuprg  4642  prssg  4757  ssunsn2  4765  eqsn  4767  prneimg2  4793  preqsnd  4797  2ralunsn  4833  eluniab  4859  csbuni  4875  elintabg  4895  dfiin2g  4967  disjprg  5075  disjxun  5077  cbvopab1g  5154  cbvmptfg  5180  al0ssb  5237  reusv3  5341  elopg  5413  opthneg  5428  opeqsng  5451  sotrieq2  5565  frsn  5713  eliunxp  5786  exopxfr2  5793  relop  5799  eldm2g  5848  reldm0  5877  relrn0  5922  restidsing  6012  elimasng  6048  asymref2  6074  somin1  6090  imadifssran  6109  xpnz  6117  xpcan  6134  xpcan2  6135  relsn2  6170  dfpo2  6254  ordtri2  6352  ordtri3  6353  oneqmini  6370  cbviota  6457  iotaval2  6463  iota1  6471  sniota  6483  fncnv  6565  fnres  6619  sbcfng  6659  sbcfg  6660  brprcneu  6824  brprcneuALT  6825  fnopfvb  6885  fvelrnb  6894  funimass4  6898  unima  6909  dffv2  6929  fvopab3g  6937  eqfnfv  6978  eqfnfv3  6980  eqfnfv2f  6982  fvreseq0  6986  fnreseql  6996  fniniseg  7008  respreima  7014  rexrn  7035  ralrn  7036  f1ompt  7059  fssrescdmd  7075  fsn  7084  funopsn  7097  funopsnOLD  7098  funsndifnop  7101  fprb  7145  tpres  7152  eufnfv  7180  ralima  7188  reximaOLD  7190  ralimaOLD  7191  dff13  7205  f13dfv  7225  fliftfun  7263  isocnv  7281  isoini  7289  f1oiso  7302  fnssintima  7313  imaeqsexvOLD  7314  cbvriota  7333  riotaeqimp  7346  eusvobj2  7355  oprabidw  7394  oprabid  7395  f1opr  7419  eloprabga  7472  resoprab  7481  eqfnov  7492  eqfnov2  7493  ov6g  7527  ovelrn  7539  funimassov  7540  ovelimab  7541  ndmovg  7546  caovord2  7575  imaeqexov  7601  imaeqalov  7602  tfisi  7806  eqop  7980  releldm2  7992  dfoprab4  8004  opiota  8008  bropopvvv  8036  bropfvvvv  8038  fparlem1  8058  fparlem2  8059  xporderlem  8074  poxp  8075  soxp  8076  fnwelem  8078  xpord2lem  8089  poxp2  8090  frxp2  8091  xpord2indlem  8094  poxp3  8097  frxp3  8098  xpord3pred  8099  xpord3inddlem  8101  elsuppfng  8116  elsuppfn  8117  rexsupp  8129  suppcoss  8154  mpoxopovel  8167  brtpos2  8179  brtpos0  8180  rntpos  8186  dftpos3  8191  tpostpos  8193  tpossym  8205  tposoprab  8209  mpocurryd  8216  frrlem1  8233  oevn0  8447  om00el  8508  omordlim  8509  omlimcl  8510  oeoa  8530  oeoe  8532  oeeulem  8534  oeeui  8535  oaabs2  8582  omabs  8584  cofonr  8607  naddunif  8626  naddasslem1  8627  naddasslem2  8628  erth2  8696  qliftfun  8746  erovlem  8757  ecopovsym  8763  mapdm0  8786  elpmg  8787  elpm2g  8788  dom2lem  8936  mapsnend  8980  xpdom2  9007  omxpenlem  9013  0sdomg  9041  fodomr  9063  xpf1o  9074  mapen  9076  ac6sfi  9191  fodomfir  9235  mapfien  9318  marypha2lem3  9347  ordtypelem7  9436  wemaplem1  9458  wemapsolem  9462  elharval  9473  brwdom3  9494  unwdomg  9496  xpwdomg  9497  inf3lem1  9547  cantnfs  9585  cantnfp1lem2  9598  cantnflem1d  9607  cantnflem1  9608  wemapwe  9616  ssttrcl  9634  ttrcltr  9635  ttrclss  9639  ttrclselem2  9645  r1sdom  9696  rankr1ai  9720  rankval2  9740  unbndrank  9764  rankunb  9772  tcrank  9806  bnd2  9815  cardnueq0  9886  iscard2  9898  r0weon  9932  fseqenlem1  9944  alephord2  9996  cardaleph  10009  aceq0  10038  dfac5lem4OLD  10048  dfac5  10049  kmlem14  10084  cfsmolem  10190  isfin4-2  10234  fin23lem26  10245  fin23lem22  10247  fin1a2lem7  10326  axdc3lem2  10371  axdc3  10374  zfac  10380  zornn0g  10425  axdclem  10439  brdom3  10448  zfcndac  10540  fpwwe2lem7  10558  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  pwfseqlem3  10581  winainflem  10614  eltsk2g  10672  inatsk  10699  axgroth2  10746  axgroth6  10749  sstskm  10763  ltexpi  10823  ordpinq  10864  lterpq  10891  ltanq  10892  ltmnq  10893  genpv  10920  genpelv  10921  prlem934  10954  prlem936  10968  addcmpblnr  10990  ltsrpr  10998  ltsosr  11015  mulgt0sr  11026  supsrlem  11032  elreal2  11053  ltresr  11061  ltresr2  11062  axrrecex  11084  axpre-ltadd  11088  axpre-mulgt0  11089  axpre-sup  11090  subcan2  11417  negcon1  11444  negcon2  11445  lt0neg1  11654  lt0neg2  11655  le0neg1  11656  le0neg2  11657  msq0d  11798  mulcan2g  11802  divmul2  11811  reclt1  12049  recgt1  12050  infm3  12113  suprlub  12118  suprleub  12120  infregelb  12138  ind1a  12168  addltmul  12411  arch  12432  elznn0  12537  nn0lt2  12590  eluz1  12790  raluz  12844  rexuz  12846  nnwof  12862  cnref1o  12933  ltxr  13064  xrltlen  13095  dflt2  13097  xrrebnd  13118  xlt0neg1  13169  xlt0neg2  13170  xle0neg1  13171  xle0neg2  13172  xmulneg1  13219  supxrbnd  13278  elixx1  13305  ixxun  13312  elioo2  13337  elicc4  13364  elioopnf  13394  elioomnf  13395  iccneg  13423  iccshftr  13437  iccshftl  13439  iccdil  13441  icccntr  13443  iccf1o  13447  elfz1  13464  0fz1  13496  elfzp1  13526  fzpr  13531  uzsplit  13548  elfzm1b  13554  elfzp12  13555  fznn0  13571  fvinim0ffz  13742  injresinj  13744  fleqceilz  13811  zmodid2  13856  fsuppmapnn0fiub0  13953  bernneq  14189  hasheqf1o  14309  euhash1  14380  hashbclem  14412  hashfacen  14414  hashf1  14417  hashge2el2difr  14441  hashtpg  14445  ccatrn  14550  pfxsuffeqwrdeq  14658  wrd2ind  14683  scshwfzeqfzo  14786  wwlktovf1  14917  brtrclfv  14962  2shfti  15040  sqrtmsq2i  15348  limsupgle  15437  limsuple  15438  rlim  15455  clim0  15466  ello12  15476  elo12  15487  o1lo1  15497  rlimresb  15525  lo1add  15587  lo1mul  15588  rlimno1  15614  summo  15677  fsumsplit  15701  mertenslem2  15848  prodmo  15899  fprodsplit  15929  fprod2dlem  15943  cnso  16212  sqrt2irr  16214  dvdsval2  16222  alzdvds  16287  odd2np1lem  16307  even2n  16309  sumodd  16355  divalgb  16371  divalgmod  16373  bitsval  16391  bitsmod  16403  sadcp1  16422  gcddvds  16470  bezoutlem3  16508  bezout  16510  lcmfunsnlem2  16607  isprm3  16650  prmind2  16652  dvdsprime  16654  ge2nprmge4  16669  coprm  16679  prmdvdsexp  16683  crth  16746  pythagtriplem2  16786  pythagtrip  16803  pceu  16815  pc11  16849  vdwapval  16942  vdwapun  16943  vdwlem10  16959  vdwlem12  16961  vdwlem13  16962  ramval  16977  ramub1lem2  16996  prmlem0  17074  elrest  17388  imasleval  17503  ismri  17595  isacs  17615  isacs2  17617  acsfn1  17625  iscatd2  17645  homfeq  17658  catpropd  17673  ismon  17698  issect  17718  issect2  17719  isinv  17725  cic  17764  isssc  17785  isfunc  17829  funcres2b  17862  isnat  17915  fucinv  17941  iszeroo  17963  elhoma  17997  setcinv  18055  isprs  18260  isdrs  18265  lubeldm  18315  glbeldm  18328  istos  18380  tosso  18381  latnle  18437  latdisd  18461  isdlat  18486  isipodrs  18501  isacs5  18512  chnccat  18590  ismgmhm  18662  issubmgm  18668  ismhm  18751  issubm  18769  issubmndb  18771  sursubmefmnd  18862  injsubmefmnd  18863  grpsubeq0  19000  grpsubadd  19002  issubg  19100  subgmulg  19114  issubg3  19118  isnsg  19128  eqger  19151  eqglact  19152  eqgid  19153  cycsubmel  19173  isghm  19188  isghmOLD  19189  isga  19264  gacan  19278  gaorb  19280  gastacos  19283  orbsta  19286  elcntz  19295  elcntzsn  19298  sscntz  19299  gsmsymgreq  19405  psgnunilem5  19467  psgnunilem3  19469  psgneldm2  19477  psgneu  19479  psgnfitr  19490  dfod2  19537  isslw  19581  sylow2alem2  19591  lsmelvalx  19613  lsmcom2  19628  lsmass  19642  lssnle  19647  pj1eu  19669  lsmhash  19678  efgi  19692  efgval2  19697  efgtlen  19699  efgred  19721  lsmcomx  19829  iscyggen2  19854  iscyg3  19859  gsumval3eu  19877  gsumzsplit  19900  eldprd  19979  subgdmdprd  20009  dprddisj2  20014  dprd2da  20017  dmdprdsplit2lem  20020  dmdprdsplit2  20021  dprdsplit  20023  dmdprdpr  20024  pgpfac1lem3  20052  pgpfac1lem4  20053  pgpfac1lem5  20054  srgfcl  20175  dvdsr02  20350  isunit  20351  isirred  20397  isrnghmmul  20420  isrngim  20423  c0snmgmhm  20440  isrhm  20456  isrim0  20460  isnzr2  20497  0ringnnzr  20504  subsubrng2  20543  subsubrg2  20578  issubrg3  20579  rngcinv  20616  ringcinv  20650  isdomn3  20694  drngunit  20713  issdrg  20767  isabv  20790  islmod  20861  islss  20931  ellspsn  21000  islmhm  21024  lmhmeql  21052  islbs  21073  lsmspsn  21081  lsmelval2  21082  lspprel  21091  lvecvscan2  21112  lvecinv  21113  lspsneq  21122  lspsneu  21123  lspsolvlem  21142  islpidl  21325  lidldvgen  21334  prmirredlem  21454  zrhrhmb  21492  zndvds  21531  elocv  21650  iscss  21665  pjdm  21689  ishil2  21701  isobs  21702  obslbs  21712  frlmelbas  21738  ellspd  21784  islinds  21791  islindf4  21820  aspval2  21880  mplsubglem  21980  mpllsslem  21981  mplmonmul  22019  opsrtoslem2  22039  ismhp  22135  mat1dimelbas  22461  dmatel  22483  scmatel  22495  mdetunilem8  22609  mdetunilem9  22610  maducoeval2  22630  cramer0  22680  cpmatel  22701  istop2g  22886  istopon  22902  toprntopon  22915  isbasis2g  22938  isbasis3g  22939  tgss2  22977  bastop1  22983  iscld  23017  elcls  23063  ntreq0  23067  isclo  23077  isclo2  23078  islp  23130  lpdifsn  23133  islpi  23139  restsn  23160  restlp  23173  ordtbaslem  23178  ordtbas2  23181  lmbr  23248  cnprest2  23280  ist0-3  23335  ist1-2  23337  cmpsublem  23389  cmpfi  23398  1stcrest  23443  2ndcdisj  23446  1stccnp  23452  llyi  23464  nllyi  23465  lly1stc  23486  iskgen3  23539  kgencn  23546  txbas  23557  eltx  23558  elpt  23562  xkoccn  23609  ptcnplem  23611  hausdiag  23635  hauseqlcld  23636  txlm  23638  txkgen  23642  kqfvima  23720  kqt0lem  23726  r0cld  23728  regr1lem2  23730  hmeoimaf1o  23760  isfbas2  23825  fbssfi  23827  trfbas2  23833  trfil2  23877  fmfnfmlem4  23947  elflim2  23954  flimrest  23973  cnflf  23992  txflf  23996  fclsopn  24004  ufilcmp  24022  cnfcf  24032  alexsubALTlem4  24040  cnextf  24056  tmdcn2  24079  qustgpopn  24110  qustgplem  24111  eltsms  24123  tsmsgsum  24129  tsmssplit  24142  elutop  24223  ustuqtop  24236  utopsnneiplem  24237  isusp  24251  isucn  24267  iscfilu  24277  ispsmet  24294  ismet  24313  isxmet  24314  metn0  24350  elblps  24377  elbl  24378  metrest  24514  metuel2  24555  psmetutop  24557  restmetu  24560  dscmet  24562  nrmmetd  24564  isngp3  24588  nmogelb  24706  isnmhm  24736  qtopbaslem  24748  xrsxmet  24800  icccmplem2  24814  metdseq0  24845  elcncf  24881  cnheibor  24947  ishtpy  24964  isphtpy  24973  isphtpc  24986  om1elbas  25024  elpi1  25037  isclmp  25089  nmhmcn  25112  iscph  25162  tcphcph  25229  lmmbrf  25254  iscfil  25257  iscfil2  25258  iscau  25268  caucfil  25275  iscmet  25276  iscmet3  25285  cfilucfil3  25312  bcthlem1  25316  rrxcph  25384  minveclem3b  25420  minveclem6  25426  evthicc2  25452  ovolfioo  25459  ovolficc  25460  ovolshftlem1  25501  ovolscalem1  25505  iundisj2  25541  dyadmbl  25592  volsup2  25597  mbfmax  25641  mbfsup  25656  mbfinf  25657  i1f1lem  25681  i1fres  25697  itg1climres  25706  itg2leub  25726  itg2seq  25734  itg2splitlem  25740  itg2monolem1  25742  itg2mono  25745  itg2cn  25755  iblpos  25785  iblcn  25791  itgsplit  25828  ellimc2  25869  dvreslem  25901  elcpn  25926  rolle  25982  dvlip  25985  dvivth  26002  tdeglem4  26050  mdegleb  26054  deg1ldg  26082  ply1nzb  26113  ply1divmo  26126  ply1divex  26127  fta1glem2  26159  plyco0  26182  elply  26185  coeeu  26215  plydivex  26288  taylthlem2  26364  radcnvlt1  26408  sincosq1sgn  26487  sincosq2sgn  26488  coseq1  26514  logreclem  26751  affineequiv  26812  affineequiv4  26815  dcubic  26835  quart  26850  atans2  26920  efrlim  26958  mumullem2  27168  dvdsflsumcom  27176  fsumvma2  27202  chpchtsum  27207  chpub  27208  dchrelbas  27224  dchrelbas2  27225  dchreq  27246  dchrptlem2  27253  gausslemma2dlem0i  27352  lgsquadlem2  27369  m1lgs  27376  2lgsoddprmlem3  27402  2sqlem6  27411  2sqlem9  27415  2sqlem10  27416  2sq2  27421  2sqreunnltb  27449  2sqreuop  27450  2sqreuopnn  27451  2sqreuoplt  27452  2sqreuopltb  27453  2sqreuopnnlt  27454  2sqreuopnnltb  27455  2sqreuopb  27456  dchrisum0flb  27498  pntpbnd1  27574  pntlem3  27597  pntlemp  27598  ltsval2  27645  ltsintdifex  27650  ltsres  27651  noextenddif  27657  nosepssdm  27675  nosupprefixmo  27689  noinfprefixmo  27690  nosupcbv  27691  nosupno  27692  nosupbnd1lem1  27697  noinfcbv  27706  noinfno  27707  noinfdm  27708  noinfres  27711  noinfbnd1lem1  27712  lestri3  27744  cutbdaylt  27815  ltsrec  27818  elold  27876  sltsleft  27877  sltsright  27878  madebdayim  27905  madebdaylemlrcut  27916  madebday  27917  newbday  27919  ltslpss  27925  cofcutr  27941  cofcutrtime  27944  addsval2  27980  addsrid  27981  addsprop  27993  negsprop  28052  lt0negs2d  28068  subadds  28087  mulsval2lem  28127  mulsrid  28130  mulsprop  28147  mulscom  28156  mulsunif2  28187  mulscan2d  28196  precsexlemcbv  28223  precsexlem9  28232  recsex  28236  absnegs  28264  onsfi  28373  n0lts1e0  28385  bdayn0p1  28386  bdayn0sf1o  28387  dfnns2  28389  eucliddivs  28393  elnnzs  28418  elznns  28419  n0seo  28438  pw2recs  28455  avglts1d  28470  avglts2d  28471  bdaypw2n0bndlem  28480  bdayfinbndcbv  28483  bdayfinbndlem1  28484  bdayfinbndlem2  28485  z12bdaylem1  28487  z12zsodd  28499  z12bday  28502  bdayfin  28504  recut  28511  renegscl  28515  remulscl  28519  istrkg2ld  28553  iscgrg  28605  tgcgr4  28624  isismt  28627  tgellng  28646  tgcolg  28647  legov  28678  lnhl  28708  lmimid  28887  iscgra1  28903  ttgelitv  28976  elee  28987  mpteleeOLD  28989  colinearalglem2  29001  colinearalg  29004  ax5seglem5  29027  axeuclidlem  29056  axeuclid  29057  axcontlem1  29058  axcontlem2  29059  axcontlem5  29062  axcontlem7  29064  wrdupgr  29179  wrdumgr  29191  uhgrspansubgrlem  29384  nbgrel  29434  nbupgrel  29439  nbgr2vtx1edg  29444  nbuhgr2vtx1edgblem  29445  nbuhgr2vtx1edgb  29446  nb3grprlem2  29475  nb3grpr2  29477  uvtx01vtx  29491  uvtxusgrel  29497  iscplgr  29509  vtxdun  29575  fusgrn0degnn0  29593  1loopgrnb0  29596  umgr2v2enb1  29620  vdiscusgrb  29624  wlkl1loop  29731  wlkv0  29743  wlklenvclwlk  29747  upgr2wlk  29760  wlkp1lem8  29772  upgrtrls  29793  upgristrl  29794  dfpth2  29822  isspthonpth  29842  usgr2trlncl  29853  usgr2pthlem  29856  usgr2pth  29857  pthdlem1  29859  isclwlke  29870  isclwlkupgr  29871  uspgrn2crct  29901  wwlks  29928  iswwlksn  29931  wwlksnext  29986  wwlksnextinj  29992  wspn0  30017  wpthswwlks2on  30057  rusgrnumwwlkl1  30064  rusgrnumwwlkslem  30065  rusgrnumwwlkb0  30067  clwlkclwwlk  30097  clwwlknwwlksn  30133  clwwlkn2  30139  clwwlkel  30141  clwwlkwwlksb  30149  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  clwwlknon1loop  30193  0wlk  30211  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  dfconngr1  30283  vdn0conngrumgrv2  30291  eupth2lem2  30314  eupth2lem3lem6  30328  eucrct2eupth  30340  isfrgr  30355  frgr3v  30370  frgrncvvdeqlem3  30396  frgrncvvdeqlem6  30399  frgrwopreglem2  30408  fusgreg2wsplem  30428  2clwwlkel  30444  extwwlkfabel  30448  numclwwlk1lem2f1  30452  numclwwlk1lem2fo  30453  numclwwlk2lem1  30471  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  nrt2irr  30568  isgrpo  30593  isssp  30820  islno  30849  nmogtmnf  30866  nmoubi  30868  nmounbi  30872  isblo  30878  ishmo  30907  ubthlem1  30966  ubthlem2  30967  minvecolem5  30977  minvecolem6  30978  hvmulcan2  31169  hire  31190  ocel  31377  ocsh  31379  pjhthmo  31398  shscom  31415  shmodsi  31485  elspani  31639  adjsym  31929  eigorthi  31933  nmopgtmnf  31964  adjeu  31985  adjval2  31987  cnvadj  31988  nmopub  32004  nmfnleub  32021  eleigvec  32053  nmop0h  32087  largei  32363  mdbr2  32392  mddmd2  32405  mdsl2i  32418  chrelat3  32467  atnemeq0  32473  chirredlem1  32486  sumdmdii  32511  sumdmdlem  32514  dmdbr5ati  32518  cdjreui  32528  nelun  32608  tpssg  32632  disjabrex  32678  disjabrexf  32679  iundisj2f  32686  disjunsn  32690  brab2d  32704  br8d  32707  opabdm  32710  opabrn  32711  nfpconfp  32731  ofpreima  32764  funcnv5mpt  32766  suppiniseg  32785  1stpreima  32806  curry2ima  32808  f1od2  32818  fpwrelmap  32832  infxrge0gelb  32865  xnn01gt  32869  nndiffz1  32885  iundisj2fi  32896  fzo0opth  32902  sgn3da  32933  tlt3  33056  toslublem  33058  tosglblem  33060  ismnt  33069  cntzun  33167  isfxp  33256  isarchi2  33273  erler  33353  domnprodeq0  33364  qusker  33439  unitprodclb  33479  lsmsnorb  33481  lsmssass  33492  grplsm0l  33493  isprmidl  33528  ismxidl  33552  mxidlirred  33562  isrprm  33607  ufdprmidl  33631  1arithufdlem4  33637  ply1degltel  33684  ply1degleel  33685  psrmonmul  33741  vieta  33771  elirng  33877  algextdeglem8  33915  fldext2chn  33919  constrextdg2  33940  constrfiss  33942  smatrcl  33987  zarcls  34065  rhmpreimacnlem  34075  cnvordtrestixx  34104  ordtconnlem1  34115  fsumcvg4  34141  lmdvg  34144  esum2dlem  34283  braew  34433  ismbfm  34442  mbfmcnt  34459  issibf  34524  eulerpartgbij  34563  eulerpartlemgvv  34567  eulerpartlemgh  34569  elorvc  34651  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemodife  34689  reprinrn  34809  reprdifc  34818  bnj1366  35018  bnj984  35141  bnj1171  35189  bnj1253  35206  bnj1417  35230  bnj1452  35241  rankval2b  35289  axprALT2  35300  lfuhgr3  35349  subfacp1lem3  35411  subfacp1lem5  35413  subfacp1lem6  35414  erdszelem9  35428  erdszelem10  35429  erdsze2lem2  35433  iscvm  35488  cvmlift2lem10  35541  snmlval  35560  satfv1  35592  satfvsucsuc  35594  satfrnmapom  35599  satf0op  35606  satf0n0  35607  sat1el2xp  35608  fmlafvel  35614  fmlaomn0  35619  gonarlem  35623  fmla0disjsuc  35627  fmlasucdisj  35628  satffunlem1lem1  35631  satffunlem2lem1  35633  satefvfmla0  35647  sategoelfvb  35648  mclsppslem  35812  r1peuqusdeg1  35872  climuzcnv  35900  br6  35986  elintfv  35994  dfdm5  36002  dfrn5  36003  dfon2lem7  36016  dfon2  36019  dfrdg2  36022  elfuns  36142  dfiota3  36150  brimg  36164  dfrdg4  36180  btwnouttr  36253  btwnexch  36254  funtransport  36260  cgr3permute1  36277  colinearperm1  36291  brsegle  36337  outsideoftr  36358  outsideofeu  36360  funray  36369  funline  36371  lineunray  36376  lineelsb2  36377  nn0prpwlem  36551  nn0prpw  36552  fneval  36581  topfneec  36584  filnetlem4  36610  ordcmp  36676  regsfromregtco  36767  regsfromsetind  36768  bj-sblem  37198  bj-sbceqgALT  37256  bj-elgab  37293  bj-clel3gALT  37402  bj-restpw  37451  bj-elid6  37531  bj-eldiag  37537  bj-eldiag2  37538  bj-imdirco  37551  f1omptsnlem  37699  mptsnunlem  37701  topdifinfeq  37713  isbasisrelowllem1  37718  isbasisrelowllem2  37719  relowlpssretop  37727  fvineqsnf1  37773  fvineqsneu  37774  wl-ifpimpr  37829  wl-sbcom2d  37933  wl-sbalnae  37934  curf  37966  unccur  37971  phpreu  37972  finixpnum  37973  ptrest  37987  poimirlem8  37996  poimirlem17  38005  poimirlem18  38006  poimirlem20  38008  poimirlem21  38009  poimirlem23  38011  poimirlem26  38014  poimirlem27  38015  poimirlem28  38016  poimirlem31  38019  poimirlem32  38020  poimir  38021  heicant  38023  mblfinlem1  38025  ismblfin  38029  mbfresfi  38034  itg2addnclem  38039  itg2addnclem2  38040  itg2addnc  38042  itg2gt0cn  38043  ftc1anclem6  38066  unirep  38082  indexa  38101  sdclem1  38111  fdc  38113  neificl  38121  istotbnd  38137  sstotbnd2  38142  isbnd  38148  isbnd3b  38153  heibor1lem  38177  heiborlem3  38181  rrnheibor  38205  ismgmOLD  38218  rngosn3  38292  isrngohom  38333  isrngoiso  38346  iscrngo2  38365  isidl  38382  ispridl  38402  pridlidl  38403  pridlnr  38404  pridl  38405  ismaxidl  38408  maxidlidl  38409  smprngopr  38420  prnc  38435  eldmres  38645  eldmressnALTV  38647  eldmqsres  38661  ideq2  38681  opideq  38711  cnvref5  38719  raldmqseu  38733  ecun  38761  ecxrn  38774  disjressuc2  38779  disjecxrn  38780  disjecxrncnvep  38781  elrels5  38812  elrels6  38813  exeupre  38859  br2coss  38896  br1cossinres  38905  br1cossxrnres  38906  br1cossinidres  38907  br1cossincnvepres  38908  br1cossxrnidres  38909  br1cossxrncnvepres  38910  br1cosscnvxrn  38932  br1cossxrncnvssrres  38956  eldmqs1cossres  39112  erimeq2  39131  disjimdmqseq  39177  eldisjs7  39309  brabsb2  39355  prter3  39375  islshp  39472  islsat  39484  islshpat  39510  lcvexchlem1  39527  lsatnem0  39538  islfl  39553  ellkr  39582  lshpsmreu  39602  lshpkrlem3  39605  cvrval2  39767  cvrnbtwn2  39768  cvrnbtwn3  39769  isat  39779  leatb  39785  leat2  39787  cvlsupr2  39836  3dim0  39950  ps-2  39971  islln  39999  islln3  40003  llnexatN  40014  islpln  40023  islpln5  40028  lplnexatN  40056  islvol  40066  islvol5  40072  dalem-cly  40164  isline  40232  ispointN  40235  ispsubsp  40238  linepsubN  40245  elpmap  40251  isline4N  40270  elpadd  40292  paddcom  40306  pmapjoin  40345  pmapjat1  40346  llnexchb2  40362  elpclN  40385  pclcmpatN  40394  ispsubclN  40430  iswatN  40487  islhp  40489  islaut  40576  ispautN  40592  isldil  40603  isltrn  40612  isltrn2N  40613  isdilN  40647  istrnN  40650  cdlemefrs29bpre0  40889  cdleme40v  40962  istendo  41253  diaelval  41526  diaeldm  41529  dibopelvalN  41636  dibopelval2  41638  dib1dim  41658  dibglbN  41659  diblsmopel  41664  dicopelval  41670  dicelvalN  41671  dicelval3  41673  dicvalrelN  41678  diclspsn  41687  dihopelvalcpre  41741  xihopellsmN  41747  dihopellsm  41748  dih1  41779  dihglblem2aN  41786  dihglblem2N  41787  dihmeetlem4preN  41799  dihglb2  41835  dvh2dim  41938  islpolN  41976  lcfl7N  41994  lcdlss  42112  hdmap1fval  42289  hdmapfval  42320  hgmapfval  42379  hdmapglem7a  42420  hdmapoc  42424  lcmineqlem  42538  sn-iotalem  42709  cxpi11d  42821  redivmul2d  42924  fimgmcyclem  43020  fimgmcyc  43021  prjsperref  43057  isnacs  43154  mzpclval  43175  elmzpcl  43176  mzpcompact2lem  43201  eldiophb  43207  eldioph3  43216  fz1eqin  43219  diophrex  43225  eq0rabdioph  43226  rexrabdioph  43240  dvdsrabdioph  43256  eldioph4b  43257  eldioph4i  43258  elpell1qr  43293  elpell14qr  43295  elpell1234qr  43297  pell1234qrmulcl  43301  rmydioph  43460  rmxdioph  43462  aomclem8  43507  islmodfg  43515  islssfg2  43517  islnm2  43524  hbtlem2  43570  hbtlem5  43574  elmnc  43582  rngunsnply  43615  onsupmaxb  43685  orddif0suc  43714  onsucf1olem  43716  cantnf2  43771  tfsconcatb0  43790  tfsconcat0i  43791  tfsconcat00  43793  ofoafg  43800  oaun3lem1  43820  naddwordnexlem4  43847  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  en2pr  43992  elmapintrab  44021  elinintrab  44022  brfvrcld  44136  brfvrcld2  44137  iunrelexpuztr  44164  brtrclfv2  44172  rfovcnvf1od  44449  fsovrfovd  44454  or3or  44468  ntrkbimka  44483  clsk3nimkb  44485  clsk1indlem4  44489  ntrclsiso  44512  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  ntrneiiso  44536  ntrneik2  44537  ntrneix2  44538  ntrneikb  44539  ntrneixb  44540  ntrneik3  44541  ntrneix3  44542  ntrneik13  44543  ntrneix13  44544  ntrneik4w  44545  gneispace3  44578  gneispace  44579  k0004lem1  44592  mnringmulrcld  44673  mnuunid  44722  grumnud  44731  expgrowth  44780  iotasbc2  44865  e2ebind  45008  modelaxreplem3  45425  modelac8prim  45437  permaxrep  45451  permac8prim  45459  nregmodel  45462  fvelrnbf  45467  rnmptbdd  45690  rnmptbd2  45694  rnmptbd  45701  caucvgbf  45933  lmbr3v  46189  lmbr3  46191  xlimpnfxnegmnf  46258  xlimmnf  46285  xlimpnf  46286  xlimmnfmpt  46287  xlimpnfmpt  46288  dfxlim2  46292  xlimpnfxnegmnf2  46302  cncfshiftioo  46336  itgiccshift  46424  itgperiod  46425  stoweidlem31  46475  stoweidlem34  46478  stoweidlem59  46503  fourierdlem2  46553  fourierdlem3  46554  fourierdlem42  46593  fourierdlem54  46604  fourierdlem81  46631  fourierdlem87  46637  fourierdlem92  46642  fourierdlem105  46655  fourierdlem113  46663  chnsubseqwl  47325  fsetsniunop  47513  fcoresf1ob  47537  f1ocof1ob  47545  reuf1odnf  47571  euoreqb  47573  fnopafvb  47619  afvelrnb  47627  afvelrnb0  47628  dmafv2rnb  47693  dfatopafv2b  47710  fnopafv2b  47713  fun2dmnopgexmpl  47748  2ffzoeq  47792  addmodne  47814  iccpart  47892  iccpartgt  47903  fargshiftfo  47918  ichexmpl2  47946  sprvalpw  47956  sprsymrelfvlem  47966  paireqne  47987  prprvalpw  47991  prprelb  47992  prprelprb  47993  prprsprreu  47995  prprreueq  47996  nprmmul3  48005  fmtnoprmfac1lem  48043  requad2  48115  fpprel  48220  fppr2odd  48223  nnsum3primesgbe  48284  bgoldbtbndlem3  48299  bgoldbtbnd  48301  vopnbgrel  48346  upgrimpths  48401  dfgric2  48407  grtriprop  48433  isgrtri  48435  stgredgel  48449  gpgvtxel  48539  gpgvtxedg1  48556  pgnbgreunbgrlem4  48611  pgnbgreunbgr  48617  isassintop  48702  assintopcllaw  48704  rngcinvALTV  48768  ringcinvALTV  48802  eliunxp2  48826  dmatALTbasel  48894  lcoval  48904  lco0  48919  lcoel0  48920  lindslinindsimp1  48949  lindslinindsimp2  48955  lincresunit3  48973  elbigo  49043  elbigo2  49044  nnolog2flm1  49082  rrx2pnedifcoorneor  49208  rrx2pnedifcoorneorr  49209  rrx2xpref1o  49210  rrx2line  49232  rrx2linest  49234  elrrx2linest2  49237  line2ylem  49243  line2x  49246  ralbidb  49291  ralbidc  49292  brab2dd  49319  resinsnALT  49364  ipolub  49479  ipoglb  49482  catprsc  49504  catprsc2  49505  funcf2lem  49572  0funcglem  49574  0funcg2  49575  0funclem  49577  termopropd  49735  fucofulem2  49802  isthincd2lem2  49926  functhinc  49939  thincsect  49958  2arwcatlem1  50086  setc1onsubc  50093