Theorem bitrd 278

Description: Deduction form of bitri 274. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)

Hypotheses

Ref	Expression
bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	pm5.74i 270	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3		bitrd.2	. . . 4 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	3	pm5.74i 270	. . 3 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃))
5	2, 4	bitri 274	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜃))
6	5	pm5.74ri 271	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:  bitr2d  279  bitr3d  280  bitr4d  281  bitrid  282  bitrdi  286  3bitrd  304  3bitr2d  306  3bitr3d  308  3bitr4d  310  imbi12d  344  bibi12d  345  sylan9bb  510  anbi12d  631  orbi12d  917  dedlem0a  1042  3bior2fd  1477  dral1v  2365  dral1vOLD  2366  dral1  2437  dral1ALT  2438  eleq12d  2826  raleqbidva  3319  rexeqbidva  3320  raleqbid  3328  rexeqbid  3329  rmoeqd  3391  reueqd  3392  ralxpxfr2d  3599  elabd2  3625  elabgt  3627  elabg  3631  eueq3  3672  reuxfrd  3709  reuxfr1d  3711  sbc19.21g  3820  sbcrext  3832  sbcabel  3837  sseq12d  3980  psseq12d  4059  sbceq1g  4379  sbceq2g  4381  sbcco3gw  4387  sbcco3g  4392  csbie2df  4405  2nreu  4406  raldifeq  4456  raaan  4483  raaanv  4484  elimhyp2v  4557  elimhyp4v  4559  keephyp2v  4563  ralsngf  4637  reusngf  4638  reuprg0  4668  reurexprg  4670  ssunsn2  4792  prel12g  4826  opthprneg  4827  2ralunsn  4857  disjeq12d  5084  disjprgw  5105  disjprg  5106  breq123d  5124  sbcbr1g  5167  sbcbr2g  5168  mpteq12da  5195  mpteq12dva  5199  treq  5235  nalset  5275  copsex4g  5457  opeqsng  5465  frirr  5615  posn  5722  sbcrel  5741  elrelimasn  6042  elinisegg  6050  epin  6052  brcodir  6078  dfpo2  6253  elpredg  6272  predep  6289  ordtri1  6355  onunel  6427  sbcfung  6530  fneq12d  6602  feq12d  6661  feq123d  6662  sbcfng  6670  sbcfg  6671  f1osng  6830  dmfco  6942  eqfnfv2  6988  fvreseq1  6994  fndmdifeq0  6999  fneqeql2  7002  funimass3  7009  funconstss  7011  unpreima  7018  ralrnmptw  7049  ralrnmpt  7051  dffo3  7057  fmptco  7080  fressnfv  7111  fmptsnd  7120  fnunirn  7206  f1elima  7215  f12dfv  7224  f13dfv  7225  cocan1  7242  cocan2  7243  fliftf  7265  soisores  7277  isomin  7287  isoini  7288  f1oiso  7301  f1ofveu  7356  mpoeq123dva  7436  ovid  7501  ov  7504  ovg  7524  caovord2d  7568  ofrfval2  7643  offveqb  7647  elpwun  7708  ordpwsuc  7755  ordunisuc2  7785  tfindsg  7802  dfom2  7809  findsg  7841  f1oweALT  7910  reldm  7981  mposn  8040  frxp3  8088  suppval1  8103  fnsuppres  8127  fnsuppeq0  8128  suppssr  8132  mpoxopoveq  8155  mpoxopovel  8156  tpostpos  8182  mpocurryd  8205  csbfrecsg  8220  oe0m1  8472  oaord1  8503  omord  8520  omlimcl  8530  oewordi  8543  oeeui  8554  nnaordr  8572  nnaordex  8590  naddov2  8630  naddel2  8639  naddss2  8641  naddunif  8644  naddasslem1  8645  naddasslem2  8646  ereq1  8662  brdifun  8684  erth2  8705  elqsecl  8717  qliftfun  8748  brecop  8756  elmapg  8785  elpmg  8788  mapsnd  8831  ixpsnval  8845  boxcutc  8886  dom2lem  8939  xpcomco  9013  pw2f1olem  9027  nndomog  9167  nndomogOLD  9177  onomeneq  9179  0sdom1dom  9189  unfilem2  9262  domunfican  9271  indexfi  9311  funisfsupp  9318  ffsuppbi  9343  elfi2  9359  supisolem  9418  inflb  9434  hartogslem1  9487  brwdom2  9518  canthwdom  9524  infeq5i  9581  cantnfs  9611  cantnfp1lem3  9625  cantnfp1  9626  cantnflem1b  9631  cantnflem1  9634  cnfcom3lem  9648  ttrcltr  9661  r1pwALT  9791  rankxplim  9824  iscard2  9921  harsucnn  9943  infxpenc2  9967  fseqenlem1  9969  fseqdom  9971  alephnbtwn  10016  alephinit  10040  iunfictbso  10059  dfac2b  10075  dfac12lem2  10089  dfac12lem3  10090  kmlem2  10096  ackbij2lem2  10185  fin23lem23  10271  fin1a2lem2  10346  fin1a2lem4  10348  fin1a2lem9  10353  dcomex  10392  axdclem  10464  brdom7disj  10476  brdom6disj  10477  iundom2g  10485  axpownd  10546  fpwwe2lem8  10583  fpwwe2  10588  pwfseqlem1  10603  eltskm  10788  ltapi  10848  ltmpi  10849  nlt1pi  10851  indpi  10852  nqereu  10874  ordpipq  10887  ltsonq  10914  ltanq  10916  ltrnq  10924  archnq  10925  elnpi  10933  genpass  10954  addclprlem1  10961  mulclprlem  10964  1idpr  10974  prlem934  10978  prlem936  10992  reclem4pr  10995  addgt0sr  11049  sqgt0sr  11051  ltresr  11085  leloe  11250  eqlelt  11251  ltaddneg  11379  ltaddnegr  11380  negeu  11400  subadd2  11414  subcan2  11435  addrsub  11581  negn0  11593  ltadd1  11631  leadd2  11633  ltsubadd  11634  lesubadd  11636  ltaddsub2  11639  leaddsub2  11641  ltaddpos  11654  lesub2  11659  ltnegcon1  11665  ltnegcon2  11666  lenegcon1  11668  lenegcon2  11669  addge01  11674  addge02  11675  suble0  11678  leaddle0  11679  lesub0  11681  eqord2  11695  sublt0d  11790  mulcan2d  11798  mulcan2g  11818  diveq0  11832  diveq1  11855  rdiv  11999  lineq  12001  ltmul2  12015  lemul2  12017  ltmulgt11  12024  ltmulgt12  12025  gt0div  12030  ge0div  12031  mulle0b  12035  mulsuble0b  12036  ltmuldiv  12037  ltdiv2  12050  ltrec1  12051  lerec2  12052  ledivdiv  12053  ltdiv23  12055  lediv23  12056  creur  12156  creui  12157  ofsubeq0  12159  nn1suc  12184  nnrecl  12420  nn0sub  12472  fcdmnn0fsuppg  12481  znnsub  12558  zgt0ge1  12566  nn0le2is012  12576  btwnnz  12588  gtndiv  12589  eluz2  12778  uzwo  12845  indstr2  12861  rpneg  12956  divlt1lt  12993  divle1le  12994  nnledivrp  13036  xrleloe  13073  xnn0xadd0  13176  xltadd2  13186  xsubge0  13190  xlesubadd  13192  xmulasslem  13214  xlemul2  13220  xltmul2  13222  supxrre2  13260  elixx3g  13287  ioo0  13299  iccid  13319  ico0  13320  ioc0  13321  icc0  13322  elioc2  13337  elico2  13338  elicc2  13339  elfz2  13441  fzen  13468  fzsubel  13487  fzpr  13506  fzrevral2  13537  fzrevral3  13538  fzshftral  13539  nn0disj  13567  2ffzeq  13572  preduz  13573  fzosplitsni  13693  btwnzge0  13743  dfceil2  13754  mod0  13791  negmod0  13793  zmodidfzo  13815  nn0ennn  13894  rabssnn0fi  13901  expeq0  14008  sq11  14046  sq01  14138  hashen  14257  hashneq0  14274  hashnncl  14276  hashsdom  14291  hashunsnggt  14304  seqcoll2  14376  pr2pwpr  14390  hashge2el2dif  14391  hashge3el3dif  14397  csbwrdg  14444  wrdnval  14445  eqwrd  14457  ccat0  14476  ccats1alpha  14519  ccatws1lenp1b  14521  swrd0  14558  swrdspsleq  14565  pfxeq  14596  pfxsuffeqwrdeq  14598  pfxsuff1eqwrdeq  14599  ccatopth2  14617  wrd2ind  14623  s2eq2s1eq  14837  s2eq2seq  14838  s3eqs2s1eq  14839  s3eq3seq  14840  2swrd2eqwrdeq  14854  brcnvtrclfv  14900  cnpart  15137  01sqrexlem7  15145  sqrtneglem  15163  sqabs  15204  abslt  15211  absle  15212  absdiflt  15214  absdifle  15215  lenegsq  15217  rexfiuz  15244  rexanuz2  15246  limsupgle  15371  limsuple  15372  clim  15388  rlim  15389  clim0c  15401  rlim0  15402  rlim0lt  15403  ello12  15410  ello1mpt  15415  elo12  15421  lo1o12  15427  elo1mpt  15428  elo1mpt2  15429  o1lo1  15431  isercolllem2  15562  isercoll2  15565  zsum  15614  fsum2dlem  15666  binomlem  15725  zprod  15831  efieq  16056  sin01bnd  16078  cos01bnd  16079  dvdsval2  16150  modm1div  16159  modmulconst  16181  dvdsaddr  16196  dvdsabseq  16206  fzocongeq  16217  odd2np1  16234  oddp1d2  16251  zob  16252  oddm1d2  16253  nnoddm1d2  16279  divalglem4  16289  divalglem5  16290  divalgb  16297  modremain  16301  bits0  16319  bitsp1e  16323  bitsp1o  16324  bitscmp  16329  bitsinv1lem  16332  sadval  16347  sadcaddlem  16348  smuval  16372  smuval2  16373  dvdssq  16454  nn0seqcvgd  16457  algcvgblem  16464  lcmdvds  16495  lcmgcdeq  16499  coprmdvds  16540  qredeq  16544  congr  16551  isprm2  16569  isprm7  16595  prmdvdsexp  16602  prmdvdsexpb  16603  prmexpb  16607  prmfac1  16608  prmdvdsncoprmbd  16613  cncongrprm  16615  qnumgt0  16636  hashdvds  16658  fermltl  16667  modprminveq  16683  pcpremul  16726  pc2dvds  16762  pcz  16764  prmpwdvds  16787  prmreclem5  16803  4sqlem16  16843  vdwapun  16857  vdwmc  16861  vdwlem6  16869  ramval  16891  prmdvdsprmo  16925  prmgaplem7  16940  cshwsiun  16983  prdsbasmpt  17366  prdsleval  17373  prdsbasmpt2  17378  imasleval  17437  xpsle  17475  mrcidb2  17512  ismri  17525  mrieqvd  17532  acsfiel  17548  acsfn2  17557  catpropd  17603  ismon2  17631  isepi2  17638  isinv  17657  dfiso3  17670  invcoisoid  17689  isocoinvid  17690  cicsym  17701  isssc  17717  subsubc  17753  funcres2b  17797  funcpropd  17801  isfull  17811  isfth  17815  fullpropd  17821  isnat2  17849  fucsect  17875  fuciso  17878  isinito  17896  istermo  17897  initoeu2lem1  17914  elsetchom  17981  setcsect  17989  setciso  17991  elestrchom  18029  fullestrcsetc  18053  posi  18220  pltval3  18242  lubfval  18253  glbfval  18266  joindef  18279  meetdef  18293  tltnle  18325  latleeqj1  18354  latleeqj2  18355  latleeqm1  18370  latleeqm2  18371  ipodrsima  18444  isacs5  18451  acsficl2d  18455  mgm1  18527  gsumvalx  18545  gsumpropd  18547  gsumpropd2lem  18548  mhmpropd  18622  issubm2  18629  mndind  18652  elefmndbas2  18698  sgrp2rid2  18750  grpsubrcan  18842  grplactcnv  18864  grp1  18868  issubg  18942  eqgval  18993  conjnmzb  19057  isga  19085  gsmsymgrfixlem1  19223  f1omvdconj  19242  f1otrspeq  19243  pmtrmvd  19252  odmulg  19352  odf1o1  19368  odngen  19373  gexdvds  19380  pgpfi2  19402  isslw  19404  slwpss  19408  pgpssslw  19410  subgslw  19412  sylow2alem2  19414  fislw  19421  sylow3lem2  19424  lsmelvalm  19447  lsmdisj3a  19485  pj1eq  19496  iscmn  19585  eqgabl  19627  torsubg  19646  abl1  19658  gsumval3  19698  telgsums  19784  dprdf11  19816  dprd2da  19835  dmdprdpr  19842  ablfac1eulem  19865  pgpfac1lem2  19868  pgpfac1lem3a  19869  pgpfac1lem3  19870  srg1zr  19960  srgen1zr  19961  ringpropd  20020  dvdsrval  20088  dvdsr02  20099  unitpropd  20142  isrimOLD  20182  drngmuleq0  20253  drngpropd  20259  rngen1zr  20263  issubrg  20270  resrhm2b  20301  islmod  20382  lsmelpr  20609  lspsnne1  20637  fidomndrnglem  20814  prmirredlem  20930  prmirred  20932  domnchr  20972  znleval  20998  znchr  21006  znunithash  21008  psgnevpmb  21028  iscss2  21127  ishil2  21162  dsmmelbas  21182  frlmplusgvalb  21212  frlmvscavalb  21213  frlmvplusgscavalb  21214  ellspd  21245  islindf  21255  islbs4  21275  islinds3  21277  coe1mul2lem2  21676  coe1tm  21681  gsumply1eq  21713  matbas2d  21809  mat1dimelbas  21857  scmatmats  21897  cramer0  22076  cpmatel2  22099  decpmataa0  22154  pm2mpf1  22185  fvmptnn04if  22235  chfacfscmul0  22244  chfacfpmmul0  22248  istopg  22281  eltg  22344  eltg2  22345  tgss2  22374  bastop1  22380  bastop2  22381  iscld  22415  iscld4  22453  elcls2  22462  elcls3  22471  isclo  22475  mretopd  22480  isnei  22491  neiint  22492  neindisj2  22511  islp2  22533  islp3  22534  maxlp  22535  cldlp  22538  neitr  22568  iscn  22623  iscnp  22625  iscnp3  22632  tgcn  22640  subbascn  22642  ssidcn  22643  lmbr2  22647  lmbrf  22648  cnnei  22670  cnrest2  22674  hausnei2  22741  cmpsub  22788  tgcmp  22789  cmpfi  22796  connsuba  22808  connsub  22809  dis2ndc  22848  subislly  22869  islocfin  22905  elkgen  22924  kgencn  22944  kgencn2  22945  eltx  22956  ptpjpre1  22959  ptcnplem  23009  hausdiag  23033  xkoptsub  23042  xkoco2cn  23046  imasnopn  23078  imasncld  23079  imasncls  23080  elqtop  23085  qtopcld  23101  kqcldsat  23121  kqt0lem  23124  isr0  23125  regr1lem2  23128  ordthmeolem  23189  ptuncnv  23195  trfbas  23232  elfg  23259  trfil3  23276  trufil  23298  filufint  23308  uffix2  23312  elfm2  23336  elfm3  23338  flimtopon  23358  flimopn  23363  fbflim  23364  fbflim2  23365  flffbas  23383  flftg  23384  cnflf  23390  txflf  23394  isfcls  23397  fclstopon  23400  fclsbas  23409  fclsrest  23412  fcfnei  23423  cnfcf  23430  ptcmplem2  23441  tgphaus  23505  tgpt0  23507  qustgphaus  23511  tsmsgsum  23527  tsmsres  23532  tsmsxplem1  23541  isust  23592  elutop  23622  utopsnneiplem  23636  utopsnnei  23638  isusp  23650  isucn  23667  isucn2  23668  ucncn  23674  ispsmet  23694  ismet  23713  isxmet  23714  metn0  23750  xmetres2  23751  elbl3ps  23781  elbl3  23782  xblpnfps  23785  xblpnf  23786  elmopn2  23835  metss  23901  stdbdxmet  23908  metcnp3  23933  metcnp  23934  metcnp2  23935  metcn  23936  txmetcnp  23940  txmetcn  23941  cfilucfil2  23954  blval2  23955  metuel  23957  metuel2  23958  metucn  23964  dscopn  23966  isngp3  23991  nmeq0  24011  ngppropd  24030  ngpocelbl  24105  isnghm3  24126  isnmhm2  24153  bl2ioo  24192  metdsge  24249  metnrmlem1a  24258  addcnlem  24264  elcncf  24289  elcncf2  24290  evth  24359  elpi1  24445  isclmp  24497  nmhmcn  24520  cphipeq0  24605  ipcau2  24635  lmmbr  24659  lmmbr2  24660  iscfil2  24667  fmcfil  24673  iscau2  24678  iscau3  24679  iscau4  24680  iscauf  24681  caucfil  24684  metcld2  24708  cfilucfil4  24722  bcthlem1  24725  lssbn  24753  cmetcusp1  24754  srabn  24761  ishl2  24771  rrxcph  24793  rrxplusgvscavalb  24796  rrxmet  24809  minveclem7  24836  ivth2  24856  ovolfioo  24868  ovolficc  24869  ovolshftlem1  24910  ovolicc2lem1  24918  icombl  24965  ioombl  24966  volsup2  25006  ismbf  25029  ismbfcn  25030  ismbfcn2  25039  mbfmax  25050  mbfimaopnlem  25056  mbfaddlem  25061  mbfsup  25065  mbfinf  25066  mbflimsup  25067  i1faddlem  25094  i1fres  25107  itg1ge0a  25113  itg1climres  25116  mbfi1fseqlem4  25120  itg2leub  25136  itg2const  25142  itg2split  25151  itg2cnlem2  25164  iblcnlem1  25189  iblrelem  25192  itgss3  25216  ellimc  25274  ellimc2  25278  ellimc3  25280  limcmpt  25284  limcmpt2  25285  limcres  25287  cnplimc  25288  limcun  25296  dvreslem  25310  dvcnp  25320  dvcnvlem  25377  dveflem  25380  cmvth  25392  mdegleb  25466  mdegldg  25468  degltp1le  25475  mdegle0  25479  deg1ldg  25494  coe1mul3  25501  ply1remlem  25564  fta1glem2  25568  ply1termlem  25601  coemulc  25653  coecj  25676  plymul0or  25678  ofmulrt  25679  quotval  25689  plydivlem4  25693  plyremlem  25701  ulmcau2  25792  reeff1o  25843  sincosq2sgn  25893  sinq12gt0  25901  coseq1  25918  logltb  25992  cosarg0d  26001  argrege0  26003  tanarg  26011  affineequiv  26210  affineequiv4  26213  affineequivne  26214  dcubic1lem  26230  dcubic  26233  atandm2  26264  rlimcnp  26352  rlimcnp2  26353  xrlimcnp  26355  fsumharmonic  26398  wilthlem1  26454  ftalem7  26465  basellem3  26469  isppw2  26501  issqf  26522  sqf11  26525  mumullem2  26566  sqff1o  26568  muinv  26579  ppiublem1  26587  vmasum  26601  chpchtsum  26604  chpub  26605  dchrelbas2  26622  dchrelbas3  26623  dchrelbas4  26628  dchrinv  26646  efexple  26666  bposlem1  26669  bposlem6  26674  bposlem7  26675  lgsdilem  26709  lgsdir2lem4  26713  lgsdir2  26715  lgsne0  26720  lgsabs1  26721  gausslemma2dlem3  26753  gausslemma2dlem7  26758  lgsquad3  26772  2lgslem1a  26776  2lgslem3c  26783  2lgslem3d  26784  2lgsoddprmlem4  26800  2sqlem7  26809  2sqlem8a  26810  2sq2  26818  2sqreulem1  26831  2sqreunnlem1  26834  chtppilim  26860  dchrvmaeq0  26889  dirith  26914  ostth3  27023  nosupbnd1lem3  27095  nosupbnd1lem5  27097  noinfbnd1lem3  27110  noetalem1  27126  eqscut2  27188  elold  27242  sleadd2  27342  sltsubsub3bd  27413  mulsproplem6  27427  mulsproplem7  27428  mulsproplem8  27429  mulsproplem9  27430  istrkgl  27463  iscgrglt  27519  tgcgr4  27536  legov  27590  legov2  27591  israg  27702  isperp  27717  opphllem3  27754  hpgbr  27765  lmiopp  27807  dfcgrg2  27868  xmstrkgc  27897  brbtwn  27911  brcgr  27912  eqeelen  27916  brbtwn2  27917  colinearalglem1  27918  colinearalglem2  27919  colinearalglem3  27920  colinearalg  27922  axcgrid  27928  ax5seglem4  27944  ax5seglem5  27945  axbtwnid  27951  axcontlem5  27980  axcontlem7  27982  ecgrtg  27995  uhgreq12g  28079  isuhgrop  28084  uhgr0e  28085  wrdupgr  28099  upgrop  28108  isumgrs  28110  wrdumgr  28111  uhgrvtxedgiedgb  28150  isusgrs  28170  isuspgrop  28175  isusgrop  28176  uhgr2edg  28219  issubgr2  28283  fusgrfisbase  28339  nbusgreledg  28364  usgrnbcnvfv  28376  nb3grprlem1  28391  uvtx2vtx1edgb  28410  iscplgrnb  28427  iscplgredg  28428  iscusgredg  28434  cplgr2vpr  28444  cusgr3vnbpr  28447  cusgrfilem3  28468  sizusglecusg  28474  vtxduhgr0edgnel  28505  vtxdgfusgrf  28508  1loopgrvd0  28515  umgr2v2enb1  28537  usgruvtxvdb  28540  vdiscusgrb  28541  isrgr  28570  isrusgr0  28577  rgrusgrprc  28600  isewlk  28613  iswlk  28621  upgriswlk  28652  wlkdlem1  28693  upgrf1istrl  28714  upgrwlkdvspth  28750  isspthonpth  28760  usgr2pth  28775  usgr2pth0  28776  iswwlksnx  28848  wlknewwlksn  28895  wlknwwlksnbij  28896  umgrwwlks2on  28965  wwlks2onsym  28966  usgr2wspthons3  28972  usgr2wspthon  28973  elwspths2spth  28975  rusgrnumwwlkl1  28976  clwlkclwwlklem2a4  29004  clwlkclwwlk  29009  clwlkclwwlk2  29010  clwwlkinwwlk  29047  clwwlkf  29054  clwwlkf1  29056  clwwlknwwlksnb  29062  eclclwwlkn1  29082  clwwlkvbij  29120  0clwlkv  29138  eupth2lem2  29226  eupth2lem3lem3  29237  eupth2lem3lem7  29241  isfrgr  29267  frgr3v  29282  frgrncvvdeqlem2  29307  fusgr2wsp2nb  29341  wlkl0  29374  isgrpo  29502  isablo  29551  vciOLD  29566  isvclem  29582  nmoubi  29777  nmobndi  29780  nmoo0  29796  isph  29827  minvecolem4b  29883  minvecolem4  29885  minvecolem5  29886  minvecolem7  29888  h2hcau  29984  h2hlm  29985  hvaddeq0  30074  hial2eq2  30112  norm-i  30134  hhssnv  30269  shsel  30319  shsel3  30320  pjhtheu2  30421  chssoc  30501  chsscon1  30506  chpsscon1  30509  chpsscon2  30510  chlejb2  30518  elspansn2  30572  fh1  30623  fh2  30624  cm2j  30625  eigposi  30841  nmopub  30913  unopf1o  30921  nmfnleub  30930  elnlfn  30933  adjvalval  30942  lnopcnre  31044  riesz4i  31068  leop2  31129  leop3  31130  leoppos  31131  hst1h  31232  mdbr2  31301  mdbr3  31302  mdbr4  31303  dmdbr2  31308  dmdbr3  31310  dmdbr4  31311  mddmd2  31314  cvdmd  31342  atcvatlem  31390  atdmd  31403  sumdmdii  31420  dmdbr5ati  31427  cdj3lem1  31439  addltmulALT  31451  opsbc2ie  31468  reuxfrdf  31483  eqrrabd  31494  iuneq12daf  31542  disjunsn  31579  br8d  31596  iunsnima2  31605  elimampt  31619  2ndimaxp  31630  abfmpeld  31637  abfmpel  31638  fmptcof2  31640  ressupprn  31672  f1od2  31706  suppss3  31709  fpwrelmapffslem  31717  xeqlelt  31747  nndiffz1  31757  hashgt1  31780  posrasymb  31895  isomnd  31979  ogrpinvlt  32001  isarchi  32088  isarchi3  32093  isarchiofld  32183  ecxpid  32220  rspsnel  32232  islbs5  32240  lindfpropd  32242  elgrplsmsn  32244  grplsm0l  32257  nsgqusf1olem3  32267  ghmquskerlem1  32269  elrspunidl  32279  qsidomlem1  32301  ply1moneq  32364  ply1degltel  32365  extdg1id  32439  elirng  32447  smatrcl  32466  1smat1  32474  ist0cld  32503  lmxrge0  32622  zrhker  32647  ismntop  32696  esumlub  32748  esum2dlem  32780  issiga  32800  dya2ub  32959  elcarsg  32994  itgeq12dv  33015  oddpwdc  33043  eulerpartlemgvv  33065  eulerpartlemgh  33067  orvcgteel  33156  ballotlemfc0  33181  ballotlemfcc  33182  ballotlemrv1  33209  ballotlemrv2  33210  ballotlem1ri  33223  signswch  33262  reprpmtf1o  33328  reprdifc  33329  bnj1417  33742  bnj1452  33753  nummin  33784  derangval  33848  derangenlem  33852  subfacp1lem2a  33861  subfacp1lem5  33865  erdszelem8  33879  iccllysconn  33931  cvmsval  33947  goeleq12bg  34030  satfv1lem  34043  satfv1  34044  satfvsucsuc  34046  satfbrsuc  34047  fmlafvel  34066  satffunlem1lem2  34084  satffunlem2lem2  34087  sategoelfvb  34100  prv0  34111  prv1n  34112  untelirr  34366  untsucf  34368  untangtr  34372  fv1stcnv  34437  fv2ndcnv  34438  dfon2lem3  34446  dfon2lem4  34447  dfon2lem7  34450  cgrcomlr  34659  ifscgr  34705  cgr3permute2  34710  cgr3permute4  34711  cgr3permute5  34712  brcolinear2  34719  brcolinear  34720  colinearperm2  34725  colinearperm4  34726  colinearperm5  34727  brofs2  34738  brifs2  34739  btwnconn1lem3  34750  btwnconn1lem4  34751  btwnconn1lem5  34752  btwnconn1lem8  34755  btwnconn1lem10  34757  btwnconn1lem11  34758  brsegle2  34770  broutsideof3  34787  outsideofeu  34792  lineunray  34808  hfninf  34847  elicc3  34865  nn0prpwlem  34870  nn0prpw  34871  topfneec  34903  neibastop3  34910  neifg  34919  eltail  34922  filnetlem4  34929  nndivlub  35006  dnibndlem13  35029  unbdqndv1  35047  bj-pm11.53vw  35317  bj-equsalvwd  35321  bj-elgab  35482  bj-restuni  35641  copsex2d  35683  copsex2b  35684  opelopabbv  35687  brabd0  35691  bj-opelidres  35705  bj-idreseqb  35707  bj-elid4  35712  rdgeqoa  35914  csbfinxpg  35932  wl-ifp4impr  36011  curf  36129  uncf  36130  curunc  36133  finixpnum  36136  ltflcei  36139  lindsadd  36144  matunitlindf  36149  ptrest  36150  poimirlem2  36153  poimirlem3  36154  poimirlem4  36155  poimirlem7  36158  poimirlem17  36168  poimirlem22  36173  poimirlem23  36174  poimirlem25  36176  poimirlem27  36178  poimirlem28  36179  poimirlem29  36180  poimirlem30  36181  poimirlem31  36182  poimirlem32  36183  poimir  36184  broucube  36185  itg2addnclem2  36203  itg2addnclem3  36204  itg2gt0cn  36206  itgaddnclem2  36210  iblabsnclem  36214  ftc1anclem1  36224  ftc1anclem5  36228  ftc1anclem7  36230  dvasin  36235  areacirclem1  36239  areacirclem4  36242  areacirclem5  36243  areacirc  36244  sdclem2  36274  lmclim2  36290  0totbnd  36305  sstotbnd  36307  isbnd3b  36317  ismtyval  36332  isismty  36333  ismtyima  36335  heiborlem7  36349  heiborlem10  36352  bfplem1  36354  rrnmet  36361  rrnheibor  36369  ismrer1  36370  ismgmOLD  36382  opidon2OLD  36386  ismndo1  36405  elghomlem2OLD  36418  rngosn3  36456  rngosn4  36457  isdrngo2  36490  iscom2  36527  isidlc  36547  elrnres  36804  eldmressnALTV  36805  eldmres2  36808  relcnveq2  36857  relcnveq4  36858  eldmcnv  36879  brxrn  36909  disjecxrncnvep  36925  disjsuc2  36926  brin3  36945  br1cossres  36974  brressn  36976  eldm1cossres  36995  brcosscnv  37007  elrelscnveq2  37028  elrelscnveq4  37029  brssrres  37039  elcoeleqvrelsrel  37131  brerser  37212  erimeq2  37213  eleldisjseldisj  37264  brparts2  37307  ax12el  37477  islshpsm  37515  lrelat  37549  islshpat  37552  islshpcv  37588  ellkr  37624  lkr0f  37629  lkrsc  37632  lshpkrlem1  37645  islshpkrN  37655  lfl1dim  37656  lkrpssN  37698  ldual1dim  37701  ople0  37722  opltn0  37725  op1le  37727  opcon2b  37732  oplecon1b  37736  opltcon1b  37740  opltcon2b  37741  cmtvalN  37746  omllaw4  37781  cmt4N  37787  cmtbr3N  37789  cmtbr4N  37790  omlfh1N  37793  cvrval  37804  pats  37820  leatb  37827  atlle0  37840  atlltn0  37841  cvlatcvr1  37876  cvlatcvr2  37877  ishlat1  37887  glbconxN  37914  hlsupr2  37923  hlateq  37935  hlrelat  37938  hlrelat2  37939  cvrval5  37951  cvrexchlem  37955  atcvr0eq  37962  cvrat4  37979  3dim0  37993  3dim2  38004  2dim  38006  islln3  38046  llnexatN  38057  islpln3  38069  islpln5  38071  islvol3  38112  islvol5  38115  4atlem11  38145  4atlem12  38148  lineset  38274  psubspset  38280  ispsubsp2  38282  elpmapat  38300  pmapglbx  38305  isline3  38312  isline4N  38313  elpaddat  38340  elpadd2at  38342  pmapjoin  38388  dalawlem13  38419  ispsubcl2N  38483  lhpoc  38550  lhpmod2i2  38574  lhpmod6i1  38575  lautset  38618  pautsetN  38634  ltrnatb  38673  ltrnel  38675  ltrncnvel  38678  ltrneq  38685  trlid0b  38714  cdleme0ex2N  38760  cdleme3  38773  cdleme7  38785  cdlemefrs29bpre0  38932  cdlemg2cN  39125  cdlemg2cex  39127  cdlemk34  39446  cdlemkid3N  39469  cdlemkid4  39470  cdlemk39s  39475  cdlemk42  39477  dvhb1dimN  39522  diaord  39583  dia11N  39584  diaglbN  39591  dia1dim2  39598  dvhopellsm  39653  dibelval3  39683  dibopelval3  39684  dibeldmN  39694  dib11N  39696  dib1dim  39701  diblsmopel  39707  diclspsn  39730  dihopelvalbN  39774  dihopelvalcqat  39782  dihopelvalcpre  39784  xihopellsmN  39790  dihopellsm  39791  dihord3  39793  dihord4  39794  dih11  39801  dihglbcpreN  39836  dihmeetlem4preN  39842  dihlspsnat  39869  dihatexv2  39875  dochord2N  39907  dochord3  39908  dochkrshp2  39923  dihjatcclem4  39957  dihjat1lem  39964  dvh2dimatN  39976  lcfl2  40029  lcfl3  40030  lcfl4N  40031  lcfl7N  40037  lcfrvalsnN  40077  lcfrlem9  40086  lcdlss  40155  mapdordlem2  40173  mapd1o  40184  mapdcv  40196  mapdn0  40205  mapdindp  40207  mapdpglem3  40211  mapdpglem26  40234  mapdpglem27  40235  mapdpglem30  40238  mapdindp1  40256  lspindp5  40306  hdmapeq0  40380  hdmap11  40384  hdmapoc  40467  hlhilphllem  40499  recbothd  40523  lcmineqlem4  40562  aks6d1c2p2  40622  sticksstones1  40627  metakunt15  40664  metakunt16  40665  fsuppind  40823  fsuppssindlem2  40825  absdvdsabsb  40871  dvdsexpnn0  40885  renegeulemv  40895  sn-subeu  40953  sn-ltaddpos  40968  sn-ltaddneg  40969  reposdif  40970  relt0neg2  40972  elrfi  41075  elrfirn2  41077  isnacs2  41087  mrefg3  41089  nacsfix  41093  lzunuz  41149  diophin  41153  sbc2rexgOLD  41169  sbc4rexgOLD  41171  4rexfrabdioph  41179  6rexfrabdioph  41180  diophren  41194  fiphp3d  41200  irrapxlem2  41204  elpell1qr2  41253  reglogltb  41272  reglogleb  41273  monotuz  41323  monotoddzz  41325  zindbi  41328  rmyeq0  41335  dvdsabsmod0  41369  jm2.19lem2  41372  jm2.19lem3  41373  rmydioph  41396  expdiophlem1  41403  expdioph  41405  pw2f1o2val2  41422  soeq12d  41423  freq12d  41424  weeq12d  41425  fnwe2lem2  41436  islmodfg  41454  islssfg2  41456  pwfi2f1o  41481  islnr3  41500  rngunsnply  41558  idomrootle  41580  onsupeqnmax  41639  onsucf1o  41665  omabs2  41725  ordsssucb  41728  tfsconcatfv  41734  tfsconcatb0  41737  tfsconcat0i  41738  tfsconcat0b  41739  tfsconcatrev  41741  tfsnfin  41745  naddcnff  41755  naddcnffo  41757  naddcnfcom  41759  naddcnfid1  41760  naddcnfid2  41761  naddcnfass  41762  naddsuc2  41786  safesnsupfilb  41812  iscard4  41927  minregex  41928  brfvrcld2  42086  brtrclfv2  42121  frege124d  42155  sbcheg  42173  frege72  42329  frege91  42348  frege92  42349  rfovcnvf1od  42398  fsovcnvlem  42407  uneqsn  42419  ntrk0kbimka  42433  ntrclselnel1  42451  ntrclsneine0lem  42458  ntrclsk2  42462  ntrclskb  42463  ntrclsk13  42465  ntrclsk4  42466  ntrneifv2  42474  ntrneineine0lem  42477  ntrneineine1lem  42478  ntrneicls00  42483  ntrneicls11  42484  ntrneiiso  42485  ntrneik2  42486  ntrneix2  42487  ntrneikb  42488  ntrneik3  42490  ntrneix3  42491  ntrneik13  42492  ntrneix13  42493  ntrneik4  42495  clsneiel1  42502  clsneiel2  42503  neicvgel2  42514  extoimad  42559  mnringelbased  42616  radcnvrat  42716  caofcan  42725  pm14.122c  42826  pm14.123c  42829  sbaniota  42837  trsbc  42944  fnchoice  43356  rfcnpre3  43360  rfcnpre4  43361  dffo3f  43520  fsneq  43548  elmptima  43607  supxrre3  43680  ltdivgt1  43711  ltdiv23neg  43749  supxrunb3  43754  supxrleubrnmpt  43761  suprleubrnmpt  43777  infxrunb3rnmpt  43783  uzub  43786  leneg2d  43803  infxrgelbrnmpt  43809  leneg3d  43812  supminfxr  43819  xlenegcon1  43842  xlenegcon2  43843  rexanuz2nf  43848  mccl  43959  climinf  43967  islptre  43980  climf  43983  islpcn  44000  clim0cf  44015  climresmpt  44020  climf2  44027  limsupref  44046  limsupbnd1f  44047  limsuppnfd  44063  climinf2  44068  limsuppnf  44072  climinfmpt  44076  limsupmnflem  44081  limsupmnf  44082  limsupre2lem  44085  limsupre2  44086  limsupmnfuzlem  44087  limsupmnfuz  44088  limsupre2mpt  44091  limsupre3lem  44093  limsupre3  44094  limsupre3mpt  44095  limsupre3uzlem  44096  limsupre3uz  44097  limsupreuz  44098  limsupreuzmpt  44100  climuz  44105  limsupge  44122  liminflelimsup  44137  limsupgt  44139  liminfreuzlem  44163  liminfreuz  44164  liminflt  44166  liminflimsupclim  44168  climliminflimsup2  44170  climliminflimsup3  44171  climliminflimsup4  44172  liminfpnfuz  44177  stoweidlem7  44368  stoweidlem27  44388  stoweidlem35  44396  fourierdlem71  44538  fourierdlem103  44570  fourierdlem104  44571  sge0lefimpt  44784  meadjiun  44827  meaiunincf  44844  meaiuninc3v  44845  caragenval  44854  caragenel  44856  omessle  44859  elhoi  44903  hoidmvlelem5  44960  hoidmvle  44961  ovnhoi  44964  ovolval5  45016  vonvolmbl2  45024  issmf  45089  issmff  45095  issmfle  45106  issmfgt  45117  issmfge  45131  smfrec  45150  smfmullem2  45153  smfmul  45156  smfsuplem2  45173  smfsup  45175  smfinflem  45178  smfinf  45179  confun  45294  fcoresf1  45423  f1cof1b  45429  fnfocofob  45431  focofob  45432  f1ocof1ob2  45434  dfdfat2  45480  fnbrafvb  45506  afvelrnb  45515  dmfcoafv  45527  dfatdmfcoafv2  45606  ltsubsubaddltsub  45653  readdcnnred  45655  resubcnnred  45656  cndivrenred  45658  2ffzoeq  45680  iccelpart  45745  iccpartnel  45750  fargshiftfva  45755  ich2exprop  45783  prproropreud  45821  prprelprb  45829  prprspr2  45830  poprelb  45836  fmtnof1  45847  odz2prm2pw  45875  flsqrt  45905  quad1  45932  requad1  45934  requad2  45935  oddm1evenALTV  45987  oddp1evenALTV  45988  mogoldbblem  46032  sbgoldbaltlem1  46091  nnsum3primesle9  46106  bgoldbtbnd  46121  isomushgr  46138  isomuspgr  46146  isupwlk  46158  upgrisupwlkALT  46164  mgmpropd  46189  mgmhmpropd  46199  issubmgm2  46204  0nodd  46224  isclintop  46261  isrnghm  46310  isrngim  46322  lidlmmgm  46343  uzlidlring  46347  rngcsect  46398  rngciso  46400  rngcsectALTV  46410  rngcisoALTV  46412  ringcsect  46449  ringciso  46451  ringcsectALTV  46473  ringcisoALTV  46475  pgrpgt2nabl  46562  lco0  46628  islinindfis  46650  islindeps  46654  lindslinindsimp1  46658  lindslinindsimp2  46664  lmod1  46693  divge1b  46713  divgt1b  46714  elbigo2  46758  logblt1b  46770  logbpw2m1  46773  nnpw2pmod  46789  rrx2plord2  46928  eenglngeehlnmlem2  46944  rrx2vlinest  46947  rrx2linest  46948  rrx2linest2  46950  line2  46958  line2xlem  46959  line2x  46960  line2y  46961  itsclc0yqsol  46970  itscnhlc0xyqsol  46971  itsclc0b  46978  itsclinecirc0b  46980  itsclinecirc0in  46981  itsclquadb  46982  itscnhlinecirc02p  46991  logic1  46996  opnneieqvv  47064  lubeldm2d  47111  glbeldm2d  47112  joindm3  47122  meetdm3  47124  ipolubdm  47132  ipoglbdm  47135  isthinc  47161  functhinc  47185  prstchom2  47218  grptcmon  47236  grptcepi  47237  aacllem  47368