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 278	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  338  ibibr  369  biancomd  464  pm5.75  1026  19.17  2220  sb2ae  2501  sbcom3  2511  sbal1  2534  sbal2  2535  abeq2d  2875  cbvralfwOLD  3370  cbvralf  3372  cbvreuwOLD  3378  cbvreu  3382  cbvrabw  3425  cbvrab  3426  ralxpxfr2d  3577  clel2g  3589  clel4g  3594  elabd2  3602  ralab2  3635  rexab2  3637  reu7  3668  reu8  3669  2reu5  3694  cbvralcsf  3878  cbvreucsf  3880  cbvrabcsf  3881  ralss  3992  rexss  3993  sbcssg  4455  elpwunsn  4620  reuprg0  4639  reuprg  4640  prssg  4753  ssunsn2  4761  eqsn  4763  preqsnd  4790  2ralunsn  4827  eluniab  4855  csbuni  4871  elintab  4891  dfiun2gOLD  4962  dfiin2g  4963  disjprgw  5070  disjprg  5071  disjxun  5073  cbvopab1g  5151  cbvmptf  5184  cbvmptfg  5185  al0ssb  5233  reusv3  5329  elopg  5382  opthneg  5397  opeqsng  5418  sotrieq2  5534  frsn  5675  eliunxp  5749  exopxfr2  5756  relop  5762  eldm2g  5811  reldm0  5840  relrn0  5881  restidsing  5965  elimasng  5999  asymref2  6027  somin1  6043  xpnz  6067  xpcan  6084  xpcan2  6085  relsn2  6120  dfpo2  6203  ordtri2  6305  ordtri3  6306  oneqmini  6321  cbviota  6405  iotaval  6411  iota1  6414  sniota  6428  fncnv  6514  fnres  6568  sbcfng  6606  sbcfg  6607  brprcneu  6773  brprcneuALT  6774  fnopfvb  6832  fvelrnb  6839  funimass4  6843  unima  6852  dffv2  6872  fvopab3g  6879  eqfnfv  6918  eqfnfv3  6920  eqfnfv2f  6922  fvreseq0  6924  fnreseql  6934  fniniseg  6946  respreima  6952  rexrn  6972  ralrn  6973  f1ompt  6994  fsn  7016  funopsn  7029  funsndifnop  7032  fprb  7078  tpres  7085  eufnfv  7114  rexima  7122  ralima  7123  dff13  7137  f13dfv  7155  fliftfun  7192  isocnv  7210  isoini  7218  f1oiso  7231  cbvriota  7255  riotaeqimp  7268  eusvobj2  7277  oprabidw  7315  oprabid  7316  f1opr  7340  eloprabga  7391  eloprabgaOLD  7392  resoprab  7401  eqfnov  7412  eqfnov2  7413  ov6g  7445  ovelrn  7457  funimassov  7458  ovelimab  7459  ndmovg  7464  caovord2  7493  tfisi  7714  eqop  7882  releldm2  7893  dfoprab4  7904  opiota  7908  bropopvvv  7939  bropfvvvv  7941  fparlem1  7961  fparlem2  7962  xporderlem  7977  poxp  7978  soxp  7979  fnwelem  7981  elsuppfng  7995  elsuppfn  7996  rexsupp  8007  suppcoss  8032  mpoxopovel  8045  brtpos2  8057  brtpos0  8058  rntpos  8064  dftpos3  8069  tpostpos  8071  tpossym  8083  tposoprab  8087  mpocurryd  8094  frrlem1  8111  wfrlem1OLD  8148  oevn0  8354  om00el  8416  omordlim  8417  omlimcl  8418  oeoa  8437  oeoe  8439  oeeulem  8441  oeeui  8442  oaabs2  8488  omabs  8490  erth2  8557  qliftfun  8600  erovlem  8611  ecopovsym  8617  mapdm0  8639  elpmg  8640  elpm2g  8641  dom2lem  8789  mapsnend  8835  xpdom2  8863  omxpenlem  8869  0sdomg  8900  0sdomgOLD  8901  fodomr  8924  xpf1o  8935  mapen  8937  ac6sfi  9067  mapfien  9176  marypha2lem3  9205  ordtypelem7  9292  wemaplem1  9314  wemapsolem  9318  elharval  9329  brwdom3  9350  unwdomg  9352  xpwdomg  9353  inf3lem1  9395  cantnfs  9433  cantnfp1lem2  9446  cantnflem1d  9455  cantnflem1  9456  wemapwe  9464  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  r1sdom  9541  rankr1ai  9565  rankval2  9585  unbndrank  9609  rankunb  9617  tcrank  9651  bnd2  9660  cardnueq0  9731  iscard2  9743  r0weon  9777  fseqenlem1  9789  alephord2  9841  cardaleph  9854  aceq0  9883  dfac5lem4  9891  dfac5  9893  kmlem14  9928  cfsmolem  10035  isfin4-2  10079  fin23lem26  10090  fin23lem22  10092  fin1a2lem7  10171  axdc3lem2  10216  axdc3  10219  zfac  10225  zornn0g  10270  axdclem  10284  brdom3  10293  zfcndac  10384  fpwwe2lem7  10402  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  pwfseqlem3  10425  winainflem  10458  eltsk2g  10516  inatsk  10543  axgroth2  10590  axgroth6  10593  sstskm  10607  ltexpi  10667  ordpinq  10708  lterpq  10735  ltanq  10736  ltmnq  10737  genpv  10764  genpelv  10765  prlem934  10798  prlem936  10812  addcmpblnr  10834  ltsrpr  10842  ltsosr  10859  mulgt0sr  10870  supsrlem  10876  elreal2  10897  ltresr  10905  ltresr2  10906  axrrecex  10928  axpre-ltadd  10932  axpre-mulgt0  10933  axpre-sup  10934  subcan2  11255  negcon1  11282  negcon2  11283  lt0neg1  11490  lt0neg2  11491  le0neg1  11492  le0neg2  11493  msq0d  11633  mulcan2g  11638  divmul2  11646  reclt1  11879  recgt1  11880  infm3  11943  suprlub  11948  suprleub  11950  infregelb  11968  addltmul  12218  arch  12239  elznn0  12343  nn0lt2  12392  eluz1  12595  raluz  12645  rexuz  12647  nnwof  12663  cnref1o  12734  ltxr  12860  xrltlen  12889  dflt2  12891  xrrebnd  12911  xlt0neg1  12962  xlt0neg2  12963  xle0neg1  12964  xle0neg2  12965  xmulneg1  13012  supxrbnd  13071  elixx1  13097  ixxun  13104  elioo2  13129  elicc4  13155  elioopnf  13184  elioomnf  13185  iccneg  13213  iccshftr  13227  iccshftl  13229  iccdil  13231  icccntr  13233  iccf1o  13237  elfz1  13253  0fz1  13285  elfzp1  13315  fzpr  13320  uzsplit  13337  elfzm1b  13343  elfzp12  13344  fznn0  13357  fvinim0ffz  13515  injresinj  13517  fleqceilz  13583  zmodid2  13628  fsuppmapnn0fiub0  13722  bernneq  13953  hasheqf1o  14072  euhash1  14144  hashbclem  14173  hashfacen  14175  hashfacenOLD  14176  hashf1  14180  hashge2el2difr  14204  hashtpg  14208  ccatrn  14303  pfxsuffeqwrdeq  14420  wrd2ind  14445  scshwfzeqfzo  14548  wwlktovf1  14681  brtrclfv  14722  2shfti  14800  sqrtmsq2i  15108  limsupgle  15195  limsuple  15196  rlim  15213  clim0  15224  ello12  15234  elo12  15245  o1lo1  15255  rlimresb  15283  lo1add  15345  lo1mul  15346  rlimno1  15374  summo  15438  fsumsplit  15462  mertenslem2  15606  prodmo  15655  fprodsplit  15685  fprod2dlem  15699  cnso  15965  sqrt2irr  15967  dvdsval2  15975  alzdvds  16038  odd2np1lem  16058  even2n  16060  sumodd  16106  divalgb  16122  divalgmod  16124  bitsval  16140  bitsmod  16152  sadcp1  16171  gcddvds  16219  bezoutlem3  16258  bezout  16260  lcmfunsnlem2  16354  isprm3  16397  prmind2  16399  dvdsprime  16401  ge2nprmge4  16415  coprm  16425  prmdvdsexp  16429  prmdvdssqOLD  16433  crth  16488  pythagtriplem2  16527  pythagtrip  16544  pceu  16556  pc11  16590  vdwapval  16683  vdwapun  16684  vdwlem10  16700  vdwlem12  16702  vdwlem13  16703  ramval  16718  ramub1lem2  16737  prmlem0  16816  elrest  17147  imasleval  17261  ismri  17349  isacs  17369  isacs2  17371  acsfn1  17379  iscatd2  17399  homfeq  17412  catpropd  17427  ismon  17454  issect  17474  issect2  17475  isinv  17481  cic  17520  isssc  17541  isfunc  17588  funcres2b  17621  isnat  17672  fucinv  17700  iszeroo  17722  elhoma  17756  setcinv  17814  isprs  18024  isdrs  18028  lubeldm  18080  glbeldm  18093  istos  18145  tosso  18146  latnle  18200  latdisd  18224  isdlat  18249  isipodrs  18264  isacs5  18275  ismhm  18441  issubm  18451  issubmndb  18453  sursubmefmnd  18544  injsubmefmnd  18545  grpsubeq0  18670  grpsubadd  18672  issubg  18764  subgmulg  18778  issubg3  18782  0subg  18789  isnsg  18792  eqger  18815  eqglact  18816  eqgid  18817  cycsubmel  18828  isghm  18843  isga  18906  gacan  18920  gaorb  18922  gastacos  18925  orbsta  18928  elcntz  18937  elcntzsn  18940  sscntz  18941  gsmsymgreq  19049  psgnunilem5  19111  psgnunilem3  19113  psgneldm2  19121  psgneu  19123  psgnfitr  19134  dfod2  19180  isslw  19222  sylow2alem2  19232  lsmelvalx  19254  lsmcom2  19269  lsmass  19284  lssnle  19289  pj1eu  19311  lsmhash  19320  efgi  19334  efgval2  19339  efgtlen  19341  efgred  19363  lsmcomx  19466  iscyggen2  19490  iscyg3  19495  cygablOLD  19501  gsumval3eu  19514  gsumzsplit  19537  eldprd  19616  subgdmdprd  19646  dprddisj2  19651  dprd2da  19654  dmdprdsplit2lem  19657  dmdprdsplit2  19658  dprdsplit  19660  dmdprdpr  19661  pgpfac1lem3  19689  pgpfac1lem4  19690  pgpfac1lem5  19691  srgfcl  19760  dvdsr02  19907  isunit  19908  isirred  19950  isrhm  19974  isrim0  19976  drngunit  20005  subsubrg2  20060  issubrg3  20061  issdrg  20072  isabv  20088  islmod  20136  islss  20205  lspsnel  20274  islmhm  20298  lmhmeql  20326  islbs  20347  lsmspsn  20355  lsmelval2  20356  lspprel  20365  lvecvscan2  20383  lvecinv  20384  lspsneq  20393  lspsneu  20394  lspsolvlem  20413  islpidl  20526  lidldvgen  20535  isnzr2  20543  0ringnnzr  20549  prmirredlem  20703  zrhrhmb  20721  zndvds  20766  elocv  20882  iscss  20897  pjdm  20923  ishil2  20935  isobs  20936  obslbs  20946  frlmelbas  20972  ellspd  21018  islinds  21025  islindf4  21054  aspval2  21111  mplsubglem  21214  mpllsslem  21215  mplmonmul  21246  opsrtoslem2  21272  ismhp  21340  mat1dimelbas  21629  dmatel  21651  scmatel  21663  mdetunilem8  21777  mdetunilem9  21778  maducoeval2  21798  cramer0  21848  cpmatel  21869  istop2g  22054  istopon  22070  toprntopon  22083  isbasis2g  22107  isbasis3g  22108  tgss2  22146  bastop1  22152  iscld  22187  elcls  22233  ntreq0  22237  isclo  22247  isclo2  22248  islp  22300  lpdifsn  22303  islpi  22309  restsn  22330  restlp  22343  ordtbaslem  22348  ordtbas2  22351  lmbr  22418  cnprest2  22450  ist0-3  22505  ist1-2  22507  cmpsublem  22559  cmpfi  22568  1stcrest  22613  2ndcdisj  22616  1stccnp  22622  llyi  22634  nllyi  22635  lly1stc  22656  iskgen3  22709  kgencn  22716  txbas  22727  eltx  22728  elpt  22732  xkoccn  22779  ptcnplem  22781  hausdiag  22805  hauseqlcld  22806  txlm  22808  txkgen  22812  kqfvima  22890  kqt0lem  22896  r0cld  22898  regr1lem2  22900  hmeoimaf1o  22930  isfbas2  22995  fbssfi  22997  trfbas2  23003  trfil2  23047  fmfnfmlem4  23117  elflim2  23124  flimrest  23143  cnflf  23162  txflf  23166  fclsopn  23174  ufilcmp  23192  cnfcf  23202  alexsubALTlem4  23210  cnextf  23226  tmdcn2  23249  qustgpopn  23280  qustgplem  23281  eltsms  23293  tsmsgsum  23299  tsmssplit  23312  elutop  23394  ustuqtop  23407  utopsnneiplem  23408  isusp  23422  isucn  23439  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  metn0  23522  elblps  23549  elbl  23550  metrest  23689  metuel2  23730  psmetutop  23732  restmetu  23735  dscmet  23737  nrmmetd  23739  isngp3  23763  nmogelb  23889  isnmhm  23919  qtopbaslem  23931  xrsxmet  23981  icccmplem2  23995  metdseq0  24026  elcncf  24061  cnheibor  24127  ishtpy  24144  isphtpy  24153  isphtpc  24166  om1elbas  24204  elpi1  24217  isclmp  24269  nmhmcn  24292  iscph  24343  tcphcph  24410  lmmbrf  24435  iscfil  24438  iscfil2  24439  iscau  24449  caucfil  24456  iscmet  24457  iscmet3  24466  cfilucfil3  24493  bcthlem1  24497  rrxcph  24565  minveclem3b  24601  minveclem6  24607  evthicc2  24633  ovolfioo  24640  ovolficc  24641  ovolshftlem1  24682  ovolscalem1  24686  iundisj2  24722  dyadmbl  24773  volsup2  24778  mbfmax  24822  mbfsup  24837  mbfinf  24838  i1f1lem  24862  i1fres  24879  itg1climres  24888  itg2leub  24908  itg2seq  24916  itg2splitlem  24922  itg2monolem1  24924  itg2mono  24927  itg2cn  24937  iblpos  24966  iblcn  24972  itgsplit  25009  ellimc2  25050  dvreslem  25082  elcpn  25107  rolle  25163  dvlip  25166  dvivth  25183  tdeglem4  25233  tdeglem4OLD  25234  mdegleb  25238  deg1ldg  25266  ply1nzb  25296  ply1divmo  25309  ply1divex  25310  fta1glem2  25340  plyco0  25362  elply  25365  coeeu  25395  plydivex  25466  taylthlem2  25542  radcnvlt1  25586  sincosq1sgn  25664  sincosq2sgn  25665  coseq1  25690  logreclem  25921  affineequiv  25982  affineequiv4  25985  dcubic  26005  quart  26020  atans2  26090  efrlim  26128  mumullem2  26338  dvdsflsumcom  26346  fsumvma2  26371  chpchtsum  26376  chpub  26377  dchrelbas  26393  dchrelbas2  26394  dchreq  26415  dchrptlem2  26422  gausslemma2dlem0i  26521  lgsquadlem2  26538  m1lgs  26545  2lgsoddprmlem3  26571  2sqlem6  26580  2sqlem9  26584  2sqlem10  26585  2sq2  26590  2sqreunnltb  26618  2sqreuop  26619  2sqreuopnn  26620  2sqreuoplt  26621  2sqreuopltb  26622  2sqreuopnnlt  26623  2sqreuopnnltb  26624  2sqreuopb  26625  dchrisum0flb  26667  pntpbnd1  26743  pntlem3  26766  pntlemp  26767  istrkg2ld  26830  iscgrg  26882  tgcgr4  26901  isismt  26904  tgellng  26923  tgcolg  26924  legov  26955  lnhl  26985  lmimid  27164  iscgra1  27180  ttgelitv  27259  elee  27271  mptelee  27272  colinearalglem2  27284  colinearalg  27287  ax5seglem5  27310  axeuclidlem  27339  axeuclid  27340  axcontlem1  27341  axcontlem2  27342  axcontlem5  27345  axcontlem7  27347  wrdupgr  27464  wrdumgr  27476  usgrexmpl  27639  uhgrspansubgrlem  27666  nbgrel  27716  nbupgrel  27721  nbgr2vtx1edg  27726  nbuhgr2vtx1edgblem  27727  nbuhgr2vtx1edgb  27728  nb3grprlem2  27757  nb3grpr2  27759  uvtx01vtx  27773  uvtxusgrel  27779  iscplgr  27791  vtxdun  27857  fusgrn0degnn0  27875  1loopgrnb0  27878  umgr2v2enb1  27902  vdiscusgrb  27906  wlkl1loop  28014  wlkv0  28027  wlklenvclwlk  28031  upgr2wlk  28045  wlkp1lem8  28057  upgrtrls  28078  upgristrl  28079  isspthonpth  28126  usgr2trlncl  28137  usgr2pthlem  28140  usgr2pth  28141  pthdlem1  28143  isclwlke  28154  isclwlkupgr  28155  uspgrn2crct  28182  wwlks  28209  iswwlksn  28212  wwlksnext  28267  wwlksnextinj  28273  wspn0  28298  wpthswwlks2on  28335  rusgrnumwwlkl1  28342  rusgrnumwwlkslem  28343  rusgrnumwwlkb0  28345  clwlkclwwlk  28375  clwwlknwwlksn  28411  clwwlkn2  28417  clwwlkel  28419  clwwlkwwlksb  28427  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknon1loop  28471  0wlk  28489  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  dfconngr1  28561  vdn0conngrumgrv2  28569  eupth2lem2  28592  eupth2lem3lem6  28606  eucrct2eupth  28618  isfrgr  28633  frgr3v  28648  frgrncvvdeqlem3  28674  frgrncvvdeqlem6  28677  frgrwopreglem2  28686  fusgreg2wsplem  28706  2clwwlkel  28722  extwwlkfabel  28726  numclwwlk1lem2f1  28730  numclwwlk1lem2fo  28731  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  isgrpo  28868  isssp  29095  islno  29124  nmogtmnf  29141  nmoubi  29143  nmounbi  29147  isblo  29153  ishmo  29182  ubthlem1  29241  ubthlem2  29242  minvecolem5  29252  minvecolem6  29253  hvmulcan2  29444  hire  29465  ocel  29652  ocsh  29654  pjhthmo  29673  shscom  29690  shmodsi  29760  elspani  29914  adjsym  30204  eigorthi  30208  nmopgtmnf  30239  adjeu  30260  adjval2  30262  cnvadj  30263  nmopub  30279  nmfnleub  30296  eleigvec  30328  nmop0h  30362  largei  30638  mdbr2  30667  mddmd2  30680  mdsl2i  30693  chrelat3  30742  atnemeq0  30748  chirredlem1  30761  sumdmdii  30786  sumdmdlem  30789  dmdbr5ati  30793  cdjreui  30803  nelun  30868  disjabrex  30930  disjabrexf  30931  iundisj2f  30938  disjunsn  30942  br8d  30959  opabdm  30960  opabrn  30961  nfpconfp  30976  ofpreima  31011  funcnv5mpt  31014  suppiniseg  31029  1stpreima  31048  curry2ima  31050  f1od2  31065  fpwrelmap  31077  infxrge0gelb  31098  xnn01gt  31102  nndiffz1  31116  iundisj2fi  31127  tlt3  31257  toslublem  31259  tosglblem  31261  ismnt  31270  cntzun  31329  isarchi2  31448  qusker  31558  lsmsnorb  31588  lsmssass  31599  grplsm0l  31600  isprmidl  31622  ismxidl  31643  isrprm  31674  smatrcl  31755  zarcls  31833  rhmpreimacnlem  31843  cnvordtrestixx  31872  ordtconnlem1  31883  fsumcvg4  31909  lmdvg  31912  ind1a  31996  esum2dlem  32069  braew  32219  ismbfm  32228  mbfmcnt  32244  issibf  32309  eulerpartgbij  32348  eulerpartlemgvv  32352  eulerpartlemgh  32354  elorvc  32435  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemodife  32473  sgn3da  32517  reprinrn  32607  reprdifc  32616  bnj1366  32818  bnj984  32941  bnj1171  32989  bnj1253  33006  bnj1417  33030  bnj1452  33041  lfuhgr3  33090  subfacp1lem3  33153  subfacp1lem5  33155  subfacp1lem6  33156  erdszelem9  33170  erdszelem10  33171  erdsze2lem2  33175  iscvm  33230  cvmlift2lem10  33283  snmlval  33302  satfv1  33334  satfvsucsuc  33336  satfrnmapom  33341  satf0op  33348  satf0n0  33349  sat1el2xp  33350  fmlafvel  33356  fmlaomn0  33361  gonarlem  33365  fmla0disjsuc  33369  fmlasucdisj  33370  satffunlem1lem1  33373  satffunlem2lem1  33375  satefvfmla0  33389  sategoelfvb  33390  mclsppslem  33554  climuzcnv  33638  fnssintima  33685  imaeqsexv  33699  br6  33733  elintfv  33747  dfdm5  33756  dfrn5  33757  dfon2lem7  33774  dfon2  33777  dfrdg2  33780  xpord2lem  33798  poxp2  33799  frxp2  33800  xpord2ind  33803  poxp3  33805  frxp3  33806  xpord3pred  33807  sltval2  33868  sltintdifex  33873  sltres  33874  noextenddif  33880  nosepssdm  33898  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupno  33915  nosupbnd1lem1  33920  noinfcbv  33929  noinfno  33930  noinfdm  33931  noinfres  33934  noinfbnd1lem1  33935  sletri3  33967  scutbdaylt  34021  sltrec  34023  elold  34062  ssltleft  34063  ssltright  34064  madebdayim  34079  madebdaylemlrcut  34088  madebday  34089  newbday  34091  sltlpss  34096  cofcutr  34101  cofcutrtime  34102  addsid1  34136  elfuns  34226  dfiota3  34234  brimg  34248  dfrdg4  34262  btwnouttr  34335  btwnexch  34336  funtransport  34342  cgr3permute1  34359  colinearperm1  34373  brsegle  34419  outsideoftr  34440  outsideofeu  34442  funray  34451  funline  34453  lineunray  34458  lineelsb2  34459  nn0prpwlem  34520  nn0prpw  34521  fneval  34550  topfneec  34553  filnetlem4  34579  ordcmp  34645  bj-sblem  35037  bj-sbceqgALT  35096  bj-elgab  35136  bj-clel3gALT  35230  bj-restpw  35272  bj-elid6  35350  bj-eldiag  35356  bj-eldiag2  35357  bj-imdirco  35370  f1omptsnlem  35516  mptsnunlem  35518  topdifinfeq  35530  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlpssretop  35544  fvineqsnf1  35590  fvineqsneu  35591  wl-ifpimpr  35646  wl-sbcom2d  35725  wl-sbalnae  35726  curf  35764  unccur  35769  phpreu  35770  finixpnum  35771  ptrest  35785  poimirlem8  35794  poimirlem17  35803  poimirlem18  35804  poimirlem20  35806  poimirlem21  35807  poimirlem23  35809  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem31  35817  poimirlem32  35818  poimir  35819  heicant  35821  mblfinlem1  35823  ismblfin  35827  mbfresfi  35832  itg2addnclem  35837  itg2addnclem2  35838  itg2addnc  35840  itg2gt0cn  35841  ftc1anclem6  35864  unirep  35880  indexa  35900  sdclem1  35910  fdc  35912  neificl  35920  istotbnd  35936  sstotbnd2  35941  isbnd  35947  isbnd3b  35952  heibor1lem  35976  heiborlem3  35980  rrnheibor  36004  ismgmOLD  36017  rngosn3  36091  isrngohom  36132  isrngoiso  36145  iscrngo2  36164  isidl  36181  ispridl  36201  pridlidl  36202  pridlnr  36203  pridl  36204  ismaxidl  36207  maxidlidl  36208  smprngopr  36219  prnc  36234  eldmres  36416  eldmqsres  36429  ideq2  36450  opideq  36485  ecxrn  36524  br2coss  36568  br1cossinres  36572  br1cossxrnres  36573  br1cossinidres  36574  br1cossincnvepres  36575  br1cossxrnidres  36576  br1cossxrncnvepres  36577  br1cosscnvxrn  36599  elrels5  36614  elrels6  36615  br1cossxrncnvssrres  36633  eldmqs1cossres  36778  erim2  36796  brabsb2  36883  prter3  36903  islshp  37000  islsat  37012  islshpat  37038  lcvexchlem1  37055  lsatnem0  37066  islfl  37081  ellkr  37110  lshpsmreu  37130  lshpkrlem3  37133  cvrval2  37295  cvrnbtwn2  37296  cvrnbtwn3  37297  isat  37307  leatb  37313  leat2  37315  cvlsupr2  37364  3dim0  37478  ps-2  37499  islln  37527  islln3  37531  llnexatN  37542  islpln  37551  islpln5  37556  lplnexatN  37584  islvol  37594  islvol5  37600  dalem-cly  37692  isline  37760  ispointN  37763  ispsubsp  37766  linepsubN  37773  elpmap  37779  isline4N  37798  elpadd  37820  paddcom  37834  pmapjoin  37873  pmapjat1  37874  llnexchb2  37890  elpclN  37913  pclcmpatN  37922  ispsubclN  37958  iswatN  38015  islhp  38017  islaut  38104  ispautN  38120  isldil  38131  isltrn  38140  isltrn2N  38141  isdilN  38175  istrnN  38178  cdlemefrs29bpre0  38417  cdleme40v  38490  istendo  38781  diaelval  39054  diaeldm  39057  dibopelvalN  39164  dibopelval2  39166  dib1dim  39186  dibglbN  39187  diblsmopel  39192  dicopelval  39198  dicelvalN  39199  dicelval3  39201  dicvalrelN  39206  diclspsn  39215  dihopelvalcpre  39269  xihopellsmN  39275  dihopellsm  39276  dih1  39307  dihglblem2aN  39314  dihglblem2N  39315  dihmeetlem4preN  39327  dihglb2  39363  dvh2dim  39466  islpolN  39504  lcfl7N  39522  lcdlss  39640  hdmap1fval  39817  hdmapfval  39848  hgmapfval  39907  hdmapglem7a  39948  hdmapoc  39952  lcmineqlem  40067  metakunt1  40132  sn-iotalem  40196  iotavallem  40199  prjsperref  40452  isnacs  40533  mzpclval  40554  elmzpcl  40555  mzpcompact2lem  40580  eldiophb  40586  eldioph3  40595  fz1eqin  40598  diophrex  40604  eq0rabdioph  40605  rexrabdioph  40623  dvdsrabdioph  40639  eldioph4b  40640  eldioph4i  40641  elpell1qr  40676  elpell14qr  40678  elpell1234qr  40680  pell1234qrmulcl  40684  rmydioph  40843  rmxdioph  40845  aomclem8  40893  islmodfg  40901  islssfg2  40903  islnm2  40910  hbtlem2  40956  hbtlem5  40960  elmnc  40968  rngunsnply  41005  isdomn3  41036  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  en2pr  41161  elintabg  41189  elmapintrab  41191  elinintrab  41192  brfvrcld  41306  brfvrcld2  41307  iunrelexpuztr  41334  brtrclfv2  41342  rfovcnvf1od  41619  fsovrfovd  41624  or3or  41638  ntrkbimka  41655  clsk3nimkb  41657  clsk1indlem4  41661  ntrclsiso  41684  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ntrneiiso  41708  ntrneik2  41709  ntrneix2  41710  ntrneikb  41711  ntrneixb  41712  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  ntrneik4w  41717  gneispace3  41750  gneispace  41751  k0004lem1  41764  mnringmulrcld  41853  mnuunid  41902  grumnud  41911  expgrowth  41960  iotasbc2  42045  e2ebind  42190  fvelrnbf  42568  rnmptbdd  42797  rnmptbd2  42802  rnmptbd  42809  lmbr3v  43293  lmbr3  43295  xlimpnfxnegmnf  43362  xlimmnf  43389  xlimpnf  43390  xlimmnfmpt  43391  xlimpnfmpt  43392  dfxlim2  43396  xlimpnfxnegmnf2  43406  cncfshiftioo  43440  itgiccshift  43528  itgperiod  43529  stoweidlem31  43579  stoweidlem34  43582  stoweidlem59  43607  fourierdlem2  43657  fourierdlem3  43658  fourierdlem42  43697  fourierdlem54  43708  fourierdlem81  43735  fourierdlem87  43741  fourierdlem92  43746  fourierdlem105  43759  fourierdlem113  43767  fsetsniunop  44554  fcoresf1ob  44578  f1ocof1ob  44584  reuf1odnf  44610  euoreqb  44612  fnopafvb  44658  afvelrnb  44666  afvelrnb0  44667  dmafv2rnb  44732  dfatopafv2b  44749  fnopafv2b  44752  fun2dmnopgexmpl  44787  2ffzoeq  44831  iccpart  44879  iccpartgt  44890  fargshiftfo  44905  ichexmpl2  44933  sprvalpw  44943  sprsymrelfvlem  44953  paireqne  44974  prprvalpw  44978  prprelb  44979  prprelprb  44980  prprsprreu  44982  prprreueq  44983  fmtnoprmfac1lem  45027  requad2  45086  fpprel  45191  fppr2odd  45194  nnsum3primesgbe  45255  bgoldbtbndlem3  45270  bgoldbtbnd  45272  ismgmhm  45348  issubmgm  45354  isassintop  45415  assintopcllaw  45417  isrnghmmul  45462  isrngisom  45465  c0snmgmhm  45483  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  eliunxp2  45680  dmatALTbasel  45754  lcoval  45764  lco0  45779  lcoel0  45780  lindslinindsimp1  45809  lindslinindsimp2  45815  lincresunit3  45833  elbigo  45908  elbigo2  45909  nnolog2flm1  45947  rrx2pnedifcoorneor  46073  rrx2pnedifcoorneorr  46074  rrx2xpref1o  46075  rrx2line  46097  rrx2linest  46099  elrrx2linest2  46102  line2ylem  46108  line2x  46111  ralbidb  46156  ralbidc  46157  ipolub  46285  ipoglb  46288  catprsc  46305  catprsc2  46306  funcf2lem  46310  isthincd2lem2  46328  functhinc  46337  thincsect  46349