Theorem imbi12d 344

Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993.)

Hypotheses

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

Assertion

Ref	Expression
imbi12d	⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	imbi1d 341	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 340	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	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:  imbi12  346  ifpbi123d  1078  nfbiit  1852  nfbidv  1923  sbjust  2066  nfbidf  2229  cbvsbvf  2365  drnf1v  2373  drnf1  2445  mo4  2563  cbvmovw  2599  cbvmow  2600  axextg  2707  rspw  3210  cbvralvw  3211  cbvralfw  3273  raleqbidv  3313  cbvraldva2  3315  sbralie  3319  sbralieOLD  3321  cbvralf  3327  ralcom2  3344  vtoclgaf  3528  vtoclga  3529  vtocl2gafOLD  3532  vtocl3gafOLD  3534  vtocl3gaOLD  3536  vtocl4gaOLD  3539  rspct  3559  rspc  3561  rspc2gv  3583  rexraleqim  3598  ralab2  3652  nelrdva  3660  mob2  3670  mob  3672  morex  3674  reu7  3687  reu8  3688  reu2eqd  3691  cdeqim  3728  sbcimg  3786  sbcim1  3791  sbceqal  3799  csbhypf  3874  cbvralcsf  3888  dfssf  3921  reldisj  4402  ralidmw  4466  reusngf  4628  rexreusng  4633  reuprg0  4656  elpreqpr  4820  unissb  4893  intss1  4915  intmin  4920  dfiin2g  4983  dftr2c  5205  trel  5210  zfpow  5308  reusv2lem4  5343  reusv3i  5346  rext  5393  opth  5421  copsexgw  5435  copsexg  5436  poeq1  5532  pocl  5537  swopolem  5539  swopo  5540  isso2i  5566  vtoclr  5684  poinxp  5702  posn  5707  ssrel  5729  ssrel2  5731  ssrelrel  5742  relop  5796  cotrg  6064  cnvsym  6067  reu3op  6246  reuop  6247  dfpo2  6250  preddowncl  6286  frpoinsg  6297  ordelord  6335  iota5  6471  dffun2  6498  sbcfung  6512  funopg  6522  brprcneu  6820  brprcneuALT  6821  tz6.12f  6855  funbrfv  6878  ssimaexg  6916  fvmptf  6958  fvelrn  7017  fprg  7096  dff13f  7197  f1veqaeq  7198  fpropnf1  7209  f1ounsn  7214  nf1const  7246  soisores  7269  soisoi  7270  isofrlem  7282  isopolem  7287  weniso  7296  riota5f  7339  imbrov2fvoveq  7379  oprabidw  7385  oprabid  7386  f1opr  7410  ovmpos  7502  ov2gf  7503  ov3  7517  caovcan  7558  caovordig  7559  caofrss  7657  caoftrn  7659  tfisg  7792  tfis  7793  tfisi  7797  tfindsg  7799  tfindsg2  7800  tfindes  7801  dfom2  7806  limomss  7809  nnlim  7818  peano5  7831  findsg  7835  findes  7838  resf1extb  7872  f1oweALT  7912  dfoprab4f  7996  offval22  8026  f1o2ndf1  8060  frxp  8064  poxp  8066  frpoins3xpg  8078  frpoins3xp3g  8079  poxp2  8081  frxp2  8082  xpord2indlem  8085  poxp3  8088  frxp3  8089  xpord3inddlem  8092  suppfnss  8127  onfununi  8269  smoel  8288  smogt  8295  tfrlem1  8303  tz7.48lem  8368  tz7.49  8372  oawordeu  8478  omordi  8489  oeordi  8510  nnmordi  8554  omabs  8574  nneob  8579  omsmolem  8580  qsel  8728  eroveu  8744  ecopovtrn  8752  ixpsnf1o  8870  fundmeng  8963  sbth  9019  limensuc  9076  findcard  9082  findcard2  9083  findcard2d  9085  pssnn  9087  ssfi  9091  sbthfi  9117  nneneq  9124  php  9125  unxpdom  9152  findcard3  9176  ac6sfi  9177  frfi  9178  domunfican  9215  fiint  9220  iunfi  9236  finsschain  9252  dffi3  9324  marypha1lem  9326  marypha1  9327  supeq3  9342  supeq123d  9343  supmo  9345  suplub  9353  supisolem  9367  eqinf  9378  infval  9380  infmo  9390  ordiso2  9410  ordtypelem7  9419  wemaplem1  9441  wemaplem2  9442  zfregcl  9489  zfregclOLD  9490  elirrv  9492  inf0  9520  inf3lem1  9527  zfinf  9538  axinf2  9539  dfom3  9546  elom3  9547  cantnfval2  9568  cantnfle  9570  cantnflt  9571  cantnfp1lem3  9579  oemapvali  9583  cantnflem1c  9586  cantnflem1  9588  cantnf  9592  wemapwe  9596  cnfcom  9599  ttrclss  9619  ttrclselem2  9625  setind  9646  setinds  9648  frmin  9651  frinsg  9653  r1sdom  9676  r1ordg  9680  rankonidlem  9730  rankunb  9752  bnd2  9795  infxpenlem  9913  infxpenc2  9922  dfac8alem  9929  dfac8clem  9932  indcardi  9941  alephordi  9974  alephinit  9995  alephfp  10008  aceq3lem  10020  dfac5lem4  10026  dfac5lem4OLD  10028  dfac5  10029  dfac2b  10031  dfac9  10037  dfac12lem2  10045  dfac12lem3  10046  kmlem1  10051  kmlem4  10054  kmlem10  10060  kmlem12  10062  kmlem13  10063  pwsdompw  10103  ackbij1lem16  10134  cfslb2n  10168  cfsmolem  10170  sornom  10177  fin2i  10195  infpssrlem4  10206  isfin2-2  10219  isfin3ds  10229  fin23lem17  10238  fin23lem32  10244  fin23lem34  10246  fin23lem35  10247  fin23lem39  10250  fin23lem41  10252  isf32lem2  10254  isf33lem  10266  isf34lem4  10277  isf34lem6  10280  fin1a2lem10  10309  axcc2lem  10336  axcc3  10338  axcc4dom  10341  dominf  10345  axdc2lem  10348  axdc3lem2  10351  ac6sg  10388  zorn2lem7  10402  zornn0g  10405  ttukeylem5  10413  ttukeylem6  10414  axdclem  10419  dominfac  10473  axrepndlem1  10492  axrepndlem2  10493  axunndlem1  10495  axunnd  10496  axpowndlem2  10498  axpowndlem3  10499  axpowndlem4  10500  axregndlem2  10503  axregnd  10504  axinfndlem1  10505  axinfnd  10506  axacndlem4  10510  axacndlem5  10511  axacnd  10512  zfcndpow  10516  zfcndinf  10518  fpwwe2lem4  10534  fpwwe2lem7  10537  fpwwe2lem11  10541  pwfseqlem4a  10561  pwfseqlem4  10562  pwfseqlem5  10563  pwfseq  10564  wunfi  10621  wunex2  10638  inar1  10675  rankcf  10677  tskord  10680  grudomon  10717  grur1a  10719  axgroth6  10728  axgroth3  10731  axgroth4  10732  eltskm  10743  indpi  10807  pinq  10827  nqereu  10829  prcdnq  10893  prnmax  10895  ltsopr  10932  prlem936  10947  ltsosr  10994  recexsrlem  11003  mulgt0sr  11005  map2psrpr  11010  supsrlem  11011  axrrecex  11063  axpre-lttrn  11066  axpre-mulgt0  11068  axpre-sup  11069  axsup  11197  dedekind  11285  ltordlem  11651  ltord1  11652  wloglei  11658  squeeze0  12034  infm3  12090  nnsub  12178  nnunb  12386  peano5uzti  12571  fzind  12579  uzind4s  12810  uzind4s2  12811  zmax  12847  zbtwnre  12848  xmulasslem  13188  xrsupsslem  13210  xrinfmsslem  13211  xrub  13215  infmremnf  13247  injresinj  13695  om2uzlti  13861  uzindi  13893  axdc4uz  13895  ssnn0fi  13896  rabssnn0fi  13897  suppssfz  13905  seqp1  13927  seqcl2  13931  seqfveq2  13935  seqshft2  13939  monoord  13943  seqsplit  13946  seqf1olem2  13953  seqf1o  13954  seqid2  13959  seqhomo  13960  seqof2  13971  expcl2lem  13984  facdiv  14198  facwordi  14200  faclbnd4lem2  14205  hashnn0n0nn  14302  hashf1lem2  14367  seqcoll  14375  fi1uzind  14418  brfi1indALT  14421  wrdind  14633  wrd2ind  14634  swrdccatin1  14636  swrdccat3blem  14650  reuccatpfxs1lem  14657  repswccat  14697  cshf1  14721  trclfvcotr  14920  relexprelg  14949  rtrclreclem4  14972  relexpindlem  14974  ello1mpt  15432  o1co  15497  o1compt  15498  rlimcn3  15501  climcn2  15504  subcn2  15506  o1of2  15524  fsumclf  15649  fsumsplitf  15653  fsumsplit1  15656  fsum2d  15682  modfsummod  15705  fsumabs  15712  telfsumo  15713  fsumrlim  15722  fsumo1  15723  o1fsum  15724  fsumiun  15732  prodfdiv  15807  fprod2d  15892  fproddivf  15898  fprodsplitf  15899  fprodsplit1f  15901  rpnnen2lem10  16136  sqrt2irr  16162  dvdsle  16225  divalglem7  16314  divalglem8  16315  ndvdssub  16324  gcdcllem1  16414  dfgcd2  16461  algcvg  16491  algcvga  16494  algfx  16495  lcmgcdlem  16521  lcmdvds  16523  lcmf  16548  lcmfunsnlem1  16552  lcmfunsnlem2lem1  16553  lcmfunsnlem  16556  lcmfdvds  16557  lcmfun  16560  coprmgcdb  16564  coprmdvds1  16567  coprmdvds2  16569  coprmprod  16576  coprmproddvds  16578  prmind2  16600  dvdsprime  16602  nprm  16603  dvdsprm  16618  exprmfct  16619  coprm  16626  isprm6  16629  prmfac1  16635  eulerthlem2  16697  pcqmul  16769  pcqcl  16772  pc2dvds  16795  pcz  16797  prmpwdvds  16820  infpn2  16829  vdwlem12  16908  ramub2  16930  rami  16931  ramcl  16945  prmdvdsprmop  16959  prmlem0  17021  mreintcl  17501  ismred2  17509  mrissmrcd  17550  mreexexlemd  17554  iscatd2  17591  moni  17647  yoniso  18195  isprs  18206  prslem  18207  drsdirfi  18215  ispos  18224  posi  18227  isposd  18232  pospropd  18235  lubfval  18258  lublecllem  18268  glbfval  18271  joinle  18294  meetle  18308  poslubmo  18319  posglbmo  18320  resspos  18339  lubl  18422  lubun  18425  clatleglb  18428  ipodrsima  18451  acsdrsel  18453  isacs4lem  18454  isacs5lem  18455  acsdrscl  18456  mreclatBAD  18473  pslem  18482  dirtr  18512  chnind  18531  mndind  18740  mhmlem  18979  isnsg2  19072  ghmf1  19162  orbsta  19229  symgextf1  19337  gsmsymgrfix  19344  gsmsymgreq  19348  symggen  19386  psgnunilem4  19413  sylow1lem1  19514  sylow2alem2  19534  sylow2a  19535  lsmmod  19591  lsmdisj2  19598  efgsrel  19650  efgredlemd  19660  efgredlem  19663  efgred  19664  gsumzaddlem  19837  gsummptnn0fz  19902  gsummptnn0fzfv  19903  telgsumfzs  19905  telgsums  19909  dprdval  19921  dprddisj2  19957  ablfac1eulem  19990  pgpfac1lem1  19992  pgpfac1lem5  19997  pgpfac1  19998  pgpfaclem2  20000  pgpfac  20002  isomnd  20039  omndadd  20044  gsumle  20061  irredmul  20351  islring  20459  lringuplu  20463  rrgval  20616  rrgeq0i  20618  isdomn  20624  domneq0  20627  isdomn4  20635  domnlcanb  20639  domnrcanb  20641  isdrngrd  20685  isdrngrdOLD  20687  sdrgacs  20720  isorng  20780  orngmul  20784  islbs3  21096  rngqiprngimf1lem  21235  cnsubrglem  21357  prmirredlem  21413  znfld  21501  znrrg  21506  cygznlem3  21510  isphl  21569  ipeq0  21579  isphld  21595  phlpropd  21596  lsmcss  21633  frlmphl  21722  frlmup1  21739  lindfrn  21762  islindf4  21779  islindf5  21780  mplsubglem  21939  mpllsslem  21940  mplcoe1  21975  mplcoe5  21978  mpfind  22045  ismhp3  22060  coe1fzgsumd  22222  gsummoncoe1  22226  pf1ind  22273  evl1gsumd  22275  dmatelnd  22414  mat1scmat  22457  mdetdiaglem  22516  mdetralt  22526  mdetralt2  22527  mdetunilem1  22530  mdetunilem2  22531  mdetunilem3  22532  mdetunilem4  22533  mdetunilem9  22538  smadiadetr  22593  pmatcoe1fsupp  22619  mp2pm2mplem4  22727  uniopn  22815  fiinopn  22819  epttop  22927  clsndisj  22993  elcls3  23001  neiptoptop  23049  neiptopnei  23050  cnpval  23154  iscnp  23155  cnpimaex  23174  lmcvg  23180  cnprest  23207  cnprest2  23208  lmss  23216  lmff  23219  t0sep  23242  hausnei  23246  isnrm2  23276  t1sep2  23287  isreg2  23295  iscmp  23306  cmpcov  23307  cmpsublem  23317  cmpsub  23318  tgcmp  23319  uncmp  23321  fiuncmp  23322  hauscmplem  23324  cmpfi  23326  cmpfii  23327  dfconn2  23337  connsuba  23338  connsub  23339  nconnsubb  23341  1stcclb  23362  1stcfb  23363  2ndc1stc  23369  1stcrest  23371  1stcelcls  23379  restnlly  23400  lly1stc  23414  comppfsc  23450  kgenval  23453  kgeni  23455  kgencn2  23475  ptcldmpt  23532  ptclsg  23533  dfac14lem  23535  dfac14  23536  txcnp  23538  ptcnp  23540  hausdiag  23563  txlm  23566  tx1stc  23568  xkococn  23578  cnmpt12  23585  cnmpt22  23592  kqt0lem  23654  isr0  23655  regr1lem2  23658  kqreglem1  23659  r0sep  23666  ptcmpfi  23731  elmptrab  23745  isfil  23765  filss  23771  isufil2  23826  cfinufil  23846  rnelfm  23871  fmfnfmlem2  23873  fmfnfmlem4  23875  flimopn  23893  flimrest  23901  flftg  23914  cnpflf  23919  txflf  23924  fclsopni  23933  fclsrest  23942  fclscf  23943  flimfnfcls  23946  fcfnei  23953  alexsublem  23962  alexsubb  23964  alexsubALTlem3  23967  alexsubALTlem4  23968  alexsubALT  23969  cnextcn  23985  cnextfres1  23986  tgpt0  24037  qustgplem  24039  tsmsi  24052  tsmssubm  24061  tsmsres  24062  tsmsf1o  24063  tsmsxp  24073  ustssel  24124  ust0  24138  ustuqtop4  24162  ucnima  24198  ucncn  24202  iscusp  24216  cuspcvg  24218  imasdsf1olem  24291  blssps  24342  blss  24343  metss  24426  comet  24431  metcnp3  24458  metcnp2  24460  txmetcnp  24465  metuel2  24483  metucn  24489  nrmmetd  24492  nlmvscn  24605  nrginvrcn  24610  nmolb  24635  xrge0tsms  24753  divcnOLD  24787  mpomulcn  24788  divcn  24789  fsumcn  24791  elcncf2  24813  cncfi  24817  mulc1cncf  24828  cncfmet  24832  xrhmeo  24874  bndth  24887  nmoleub2lem2  25046  nmoleub3  25049  ipcn  25176  lmmbr  25188  caucfil  25213  pmltpc  25381  ovolfiniun  25432  ovolicc2lem3  25450  ovolicc2  25453  mblsplit  25463  finiunmbl  25475  volfiniun  25478  voliunlem3  25483  ioorinv  25507  ioorcl  25508  dyadmax  25529  dyadmbllem  25530  dyadmbl  25531  opnmbllem  25532  volcn  25537  vitalilem2  25540  vitalilem3  25541  vitali  25544  i1fd  25612  itg2seq  25673  itg2addlem  25689  itgfsum  25758  ellimc3  25810  dvbsss  25833  dvnres  25863  dvmptfsum  25909  dvferm1lem  25918  dvferm2lem  25920  rolle  25924  c1lip1  25932  lhop1lem  25948  lhop1  25949  dvfsumlem2  25963  dvfsumlem2OLD  25964  dvfsumlem4  25966  dvfsumrlim  25968  dvfsum2  25971  ftc1a  25974  ftc1lem6  25978  mdegleb  25999  mdeglt  26000  deg1leb  26030  deg1lt  26032  ply1divex  26072  fta1glem2  26104  fta1g  26105  plyco0  26127  plyeq0lem  26145  coeeq2  26177  dgrle  26178  dgrcolem2  26210  dgrco  26211  plydivlem4  26234  plydivex  26235  fta1lem  26245  fta1  26246  vieta1lem2  26249  vieta1  26250  aalioulem2  26271  aalioulem4  26273  abelth  26381  cxpcn3  26688  rlimcnp  26905  xrlimcnp  26908  cxploglim  26918  scvxcvx  26926  jensen  26929  lgamgulmlem2  26970  wilthlem2  27009  wilthlem3  27010  fta  27020  mpodvdsmulf1o  27134  dvdsmulf1o  27136  perfectlem2  27171  dchrelbas3  27179  dchrelbas4  27184  dchrn0  27191  bcmono  27218  lgsdir2lem4  27269  lgsdchr  27296  gausslemma2dlem0i  27305  lgseisenlem2  27317  lgsquad2lem2  27326  2sqlem6  27364  2sqlem8  27367  2sqlem10  27369  dchrisumlema  27429  dchrisumlem2  27431  dchrisumlem3  27432  nosupprefixmo  27642  noinfprefixmo  27643  nosupcbv  27644  nosupdm  27646  nosupfv  27648  nosupres  27649  nosupbnd1lem1  27650  nosupbnd1lem3  27652  nosupbnd1lem5  27654  nosupbnd2  27658  noinfcbv  27659  noinfdm  27661  noinffv  27663  noinfres  27664  noinfbnd1lem1  27665  noinfbnd1lem3  27667  noinfbnd1lem5  27669  noinfbnd2  27673  nocvxminlem  27720  madebdaylemold  27846  madebdaylemlrcut  27847  madebday  27848  lrrecpo  27887  addsproplem1  27915  addsprop  27922  sleadd1  27935  negsproplem1  27973  negsprop  27980  mulsproplemcbv  28057  mulsproplem1  28058  mulsprop  28072  precsexlem8  28155  precsexlem9  28156  precsexlem11  28158  precsex  28159  bdayon  28212  onsfi  28286  n0subs  28292  eln0zs  28327  istrkgb  28436  istrkgcb  28437  istrkge  28438  axtgcgrid  28444  axtg5seg  28446  axtgbtwnid  28447  axtgpasch  28448  axtgcont1  28449  axtgeucl  28453  iscgrglt  28495  tgcgr4  28512  axcgrtr  28897  gropd  29013  grstructd  29014  upgredg2vtx  29123  upgredgpr  29124  edglnl  29125  numedglnl  29126  usgredg2vtxeuALT  29204  nbgr2vtx1edg  29332  finsumvtxdg2size  29533  wlkp1lem8  29661  upgrwlkdvdelem  29718  usgr2wlkneq  29738  usgr2pthlem  29745  pthdlem2lem  29749  uspgrn2crct  29790  2pthdlem1  29912  eleclclwwlkn  30060  hashecclwwlkn1  30061  umgrhashecclwwlk  30062  3pthdlem1  30148  eupth2  30223  frgr3vlem1  30257  3vfriswmgrlem  30261  frgrwopreglem4a  30294  frgr2wwlk1  30313  wlkl0  30351  numclwlk2lem2f1o  30363  friendshipgt3  30382  eulplig  30469  nvz  30653  nmobndseqi  30763  nmobndseqiALT  30764  nmlno0  30779  blocnilem  30788  dipdir  30826  dipass  30829  siilem2  30836  ubthlem2  30855  ubth  30857  htth  30902  normpyth  31129  norm3lemt  31136  chlimi  31218  chcompl  31226  omlsii  31387  pjoml  31420  h1de2i  31537  elspansn2  31551  h1datom  31566  pjoml2  31595  pjoml3  31596  lecm  31601  chscllem2  31622  osum  31629  spansncv  31637  pjcjt2  31676  pjopyth  31704  eigre  31819  eigorth  31822  hhcno  31888  hhcnf  31889  cnopc  31897  cnfnc  31914  nmcexi  32010  nmcopexi  32011  nmcfnexi  32035  pjssge0i  32150  hstel2  32203  stj  32219  stri  32241  hstri  32249  stcltr1i  32258  mdbr  32278  mdi  32279  mdbr3  32281  mdbr4  32282  dmdbr  32283  dmdmd  32284  dmdi  32286  dmdbr3  32289  dmdbr4  32290  dmdbr5  32292  mdsl1i  32305  mdslmd1lem3  32311  mdslmd1lem4  32312  mdslmd1i  32313  csmdsymi  32318  cvmd  32320  atss  32330  atom1d  32337  chcv1  32339  hatomic  32344  atord  32372  atcvat2  32373  mddmdin0i  32415  opreu2reuALT  32460  rmoxfrd  32476  ifeqeqx  32526  ssiun2sf  32543  iinabrex  32553  ssrelf  32602  fmptcof2  32643  acunirnmpt  32645  acunirnmpt2  32646  acunirnmpt2f  32647  aciunf1lem  32648  suppovss  32668  fz1nntr  32791  nn0min  32810  fsumiunle  32819  wrdt2ind  32943  ressprs  32956  toslublem  32962  tosglblem  32964  mntoval  32972  ismntd  32974  dfmgc2lem  32985  dfmgc2  32986  xrge0tsmsd  33051  fzto1st  33081  psgnfzto1st  33083  submarchi  33164  archirng  33166  archiexdiv  33168  archiabllem1a  33169  archiabllem2a  33172  archiabl  33176  isarchiofld  33177  gsumvsca1  33204  gsumvsca2  33205  elrgspnlem4  33221  domnpropd  33252  domnlcanOLD  33255  linds2eq  33355  isprmidl  33412  prmidl  33414  prmidlc  33422  ssdifidlprm  33432  ismxidl  33436  mxidlmax  33439  rprmval  33490  isrprm  33491  rprmdvds  33493  rprmdvdsprod  33508  1arithidomlem1  33509  1arithidom  33511  1arithufdlem3  33520  dfufd2lem  33523  lbsdiflsp0  33662  fedgmullem1  33665  fedgmullem2  33666  fldext2chn  33764  constrmon  33780  submateq  33845  lmatfval  33850  lmatcl  33852  iscref  33880  crefi  33883  pcmplfin  33896  xrge0iifiso  33971  esumcvg  34122  esum2dlem  34128  sigaclcu  34153  sigaclci  34168  unelsiga  34170  unelldsys  34194  sigapildsys  34198  ldgenpisyslem1  34199  fiunelros  34210  measvun  34245  measiun  34254  carsgmon  34350  carsgsigalem  34351  carsgclctunlem2  34355  carsgclctun  34357  pmeasmono  34360  pmeasadd  34361  sibfof  34376  sitgclg  34378  eulerpartlemgvv  34412  signsply0  34587  signstfvneq0  34608  breprexp  34669  hgt749d  34685  istrkg2d  34702  axtgupdim2ALTV  34704  bnj1385  34867  bnj110  34893  bnj222  34918  bnj229  34919  bnj590  34945  bnj865  34958  bnj849  34960  bnj981  34985  bnj1014  34996  bnj1015  34997  bnj1112  35018  bnj1118  35019  bnj1123  35021  bnj1128  35025  bnj1125  35027  bnj1148  35031  bnj1154  35034  bnj1326  35061  bnj1384  35067  bnj1489  35091  bnj1497  35095  funen1cnv  35123  r1filimi  35137  trssfir1om  35145  r1omhfb  35146  setindregs  35151  trssfir1omregs  35155  r1omhfbregs  35156  onvf1odlem2  35171  f1resfz0f1d  35181  cplgredgex  35188  acycgrcycl  35214  subfacp1lem6  35252  erdszelem9  35266  kur14lem9  35281  sconnpht  35296  cvmsss2  35341  cvmliftlem7  35358  cvmliftlem10  35361  fmlasuc  35453  gonar  35462  goalr  35464  mclsrcl  35628  mclsssvlem  35629  mclsval  35630  mclsax  35636  mclsind  35637  mclsppslem  35650  iota5f  35791  fununiq  35836  dfon2lem3  35850  dfon2lem4  35851  dfon2lem5  35852  dfon2lem6  35853  dfon2lem7  35854  dfon2lem8  35855  dfon2  35857  btwnconn1lem11  36164  linethru  36220  fwddifnp1  36232  rankelg  36235  rankeq1o  36238  sbequbidv  36281  cbvralvw2  36293  cbvmodavw  36317  cbvsbdavw  36321  cbvsbdavw2  36322  subtr  36381  subtr2  36382  trer  36383  nn0prpwlem  36389  nn0prpw  36390  neibastop2lem  36427  filnetlem4  36448  bj-hbxfrbi  36697  bj-hbyfrbi  36698  bj-ssblem1  36721  bj-ssblem2  36722  bj-ax12  36724  irrdiff  37393  relowlssretop  37430  rdgeqoa  37437  rdgssun  37445  exrecfnlem  37446  finxpreclem6  37463  pibp19  37481  pibt2  37484  wl-ax12v2cl  37573  wl-mo3t  37643  wl-sb8mot  37647  wl-sb8motv  37648  finixpnum  37668  matunitlindflem1  37679  ptrest  37682  poimirlem13  37696  poimirlem14  37697  poimirlem17  37700  poimirlem18  37701  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem24  37707  poimirlem25  37708  poimirlem26  37709  poimirlem28  37711  poimirlem30  37713  poimirlem31  37714  poimirlem32  37715  poimir  37716  heicant  37718  mblfinlem1  37720  mblfinlem2  37721  mblfinlem3  37722  voliunnfl  37727  volsupnfl  37728  mbfresfi  37729  itg2addnclem3  37736  ftc1cnnc  37755  ftc1anclem7  37762  ftc1anc  37764  sdclem2  37805  fdc  37808  fdc1  37809  neificl  37816  mettrifi  37820  sstotbnd2  37837  cntotbnd  37859  heibor1lem  37872  bfp  37887  isass  37909  ismgmOLD  37913  isexid2  37918  iscringd  38061  ispridl  38097  pridl  38100  ismaxidl  38103  maxidlmax  38106  ispridlc  38133  pridlc  38134  dmnnzd  38138  relcnveq2  38384  ecin0  38407  elrelscnveq2  38664  elsymrels3  38673  eltrrels3  38699  eleqvrels3  38712  eqvrelqsel  38735  eldisjlem19  38931  axc11n-16  39060  ax12eq  39063  ax12el  39064  ax12inda  39070  ax12v2-o  39071  fsumshftd  39074  riotasv2d  39079  lshpdisj  39109  lsmsatcv  39132  lsat0cv  39155  lcvexchlem4  39159  lcvexchlem5  39160  l1cvpat  39176  isopos  39302  oposlem  39304  isoml  39360  omllaw  39365  isatl  39421  atlex  39438  iscvlat  39445  cvlexch1  39450  glbconN  39499  hlsuprexch  39503  ps-1  39599  3atlem5  39609  psubspi  39869  llnexchb2  39991  elpcliN  40015  pclfinclN  40072  ldilval  40235  ltrnfset  40239  ltrnset  40240  ltrnu  40243  trlfset  40282  trlset  40283  trlval2  40285  cdleme25cv  40480  cdleme31so  40501  cdleme31fv  40512  cdlemefrs29bpre0  40518  cdleme32fva  40559  cdleme40v  40591  trlord  40691  cdlemkid3N  41055  cdlemkid4  41056  dihffval  41352  dihfval  41353  dihval  41354  lpolconN  41609  mapdordlem2  41759  hdmapfval  41949  hdmapval  41950  hdmapval2  41954  aks4d1p7  42199  isprimroot  42209  primrootlekpowne0  42221  sticksstones1  42262  sticksstones2  42263  sticksstones10  42271  sticksstones12a  42273  aks6d1c6lem3  42288  indstrd  42309  unitscyglem2  42312  unitscyglem3  42313  unitscyglem4  42314  nnn1suc  42387  fsuppind  42711  eu6w  42797  ismrcd1  42818  ismrcd2  42819  ismrc  42821  isnacs3  42830  nacsfix  42832  mzpcompact2  42872  fphpd  42936  fphpdo  42937  monotuz  43061  monotoddzzfi  43062  monotoddzz  43063  oddcomabszz  43064  zindbi  43066  setindtrs  43145  dford3lem2  43147  ttac  43156  dnnumch1  43164  fnwe2lem2  43171  aomclem3  43176  aomclem6  43179  aomclem8  43181  dfac11  43182  dfac21  43186  islssfg2  43191  hbtlem5  43248  hbt  43250  flcidc  43290  mendlmod  43309  unielss  43338  rababg  43694  elmapintrab  43696  iunrelexpuztr  43839  frege92  44075  frege104  44087  ntrkbimka  44158  ntrk0kbimka  44159  neik0pk1imk0  44167  isotone1  44168  isotone2  44169  ntrclsiso  44187  ntrclskb  44189  ntrneiiso  44211  ntrneik3  44216  ntrneix3  44217  gneispacess2  44266  grur1cld  44352  scottabf  44360  ismnu  44381  mnuop23d  44386  mnuunid  44397  ismnushort  44421  dvgrat  44432  cvgdvgrat  44433  binomcxplemnotnn0  44476  pm14.122b  44543  sbiota1  44554  relprel  45071  relpfrlem  45073  modelaxreplem1  45098  modelaxreplem2  45099  modelaxrep  45101  omssaxinf2  45108  modelac8prim  45112  permaxinf2lem  45132  permac8prim  45134  nregmodel  45137  fnchoice  45153  fiiuncl  45189  iunincfi  45218  disjf1  45307  wessf1ornlem  45309  disjinfi  45316  axccdom  45346  dmrelrnrel  45350  axccd  45353  monoords  45425  fperiodmullem  45431  supxrgere  45459  supxrgelem  45463  supxrge  45464  xrlexaddrp  45478  infxr  45492  infleinf  45497  supxrleubrnmptf  45576  monoordxrv  45606  monoordxr  45607  monoord2xr  45609  fsummulc1f  45698  fsumnncl  45699  fsumf1of  45701  fsumreclf  45703  fsumlessf  45704  fsumsermpt  45706  fmul01  45707  fmulcl  45708  fmuldfeqlem1  45709  fmuldfeq  45710  fmul01lt1lem1  45711  fmul01lt1lem2  45712  fprodexp  45721  fprodabs2  45722  fprodcnlem  45726  climmulf  45731  climexp  45732  climsuse  45735  climrecf  45736  climinff  45738  climaddf  45742  mullimc  45743  mullimcf  45750  limcperiod  45755  sumnnodd  45757  lptre2pt  45765  limsupre  45766  neglimc  45772  addlimc  45773  0ellimcdiv  45774  limclner  45776  climsubmpt  45785  climreclf  45789  climeldmeqmpt  45793  climfveqmpt  45796  fnlimfvre  45799  climfveqf  45805  climfveqmpt3  45807  climeldmeqf  45808  limsupref  45810  limsupbnd1f  45811  climeqf  45813  climeldmeqmpt3  45814  climinf2  45832  limsupubuz  45838  climinf2mpt  45839  climinfmpt  45840  limsupmnf  45846  limsupequz  45848  limsupre2  45850  limsupequzmptf  45856  limsupre3  45858  lmbr3  45872  cnrefiisp  45955  xlimxrre  45956  xlimmnfvlem1  45957  xlimpnfvlem1  45961  climxlim2lem  45970  cncfshift  45999  cncfperiod  46004  icccncfext  46012  fprodcncf  46025  fperdvper  46044  dvmptmulf  46062  dvnmptdivc  46063  dvnmul  46068  dvmptfprod  46070  dvnprodlem1  46071  dvnprodlem2  46072  dvnprodlem3  46073  iblspltprt  46098  itgspltprt  46104  stoweidlem3  46128  stoweidlem4  46129  stoweidlem6  46131  stoweidlem8  46133  stoweidlem15  46140  stoweidlem16  46141  stoweidlem17  46142  stoweidlem19  46144  stoweidlem20  46145  stoweidlem22  46147  stoweidlem23  46148  stoweidlem26  46151  stoweidlem27  46152  stoweidlem30  46155  stoweidlem31  46156  stoweidlem32  46157  stoweidlem34  46159  stoweidlem35  46160  stoweidlem42  46167  stoweidlem43  46168  stoweidlem48  46173  stoweidlem50  46175  stoweidlem51  46176  stoweidlem57  46182  stoweidlem59  46184  stoweidlem62  46187  wallispilem3  46192  dirkercncflem2  46229  fourierdlem11  46243  fourierdlem12  46244  fourierdlem15  46247  fourierdlem16  46248  fourierdlem21  46253  fourierdlem34  46266  fourierdlem41  46273  fourierdlem42  46274  fourierdlem46  46277  fourierdlem48  46279  fourierdlem49  46280  fourierdlem50  46281  fourierdlem51  46282  fourierdlem68  46299  fourierdlem71  46302  fourierdlem72  46303  fourierdlem73  46304  fourierdlem76  46307  fourierdlem79  46310  fourierdlem81  46312  fourierdlem83  46314  fourierdlem86  46317  fourierdlem89  46320  fourierdlem90  46321  fourierdlem91  46322  fourierdlem92  46323  fourierdlem94  46325  fourierdlem97  46328  fourierdlem103  46334  fourierdlem104  46335  fourierdlem111  46342  fourierdlem112  46343  fourierdlem113  46344  etransclem2  46361  etransclem46  46405  salunicl  46441  saluncl  46442  intsaluni  46454  dfsalgen2  46466  sge0f1o  46507  sge0lempt  46535  sge0iunmptlemfi  46538  sge0p1  46539  sge0fodjrnlem  46541  sge0iunmpt  46543  sge0ltfirpmpt2  46551  sge0isummpt2  46557  sge0xaddlem2  46559  sge0xadd  46560  nnfoctbdjlem  46580  meadjuni  46582  meadjiun  46591  voliunsge0lem  46597  meaiuninclem  46605  meaiunincf  46608  meaiuninc3v  46609  meaiuninc3  46610  meaiininclem  46611  meaiininc  46612  omeunile  46630  isomenndlem  46655  ovn0lem  46690  ovnsubaddlem1  46695  hoidmvlelem2  46721  hoidmvlelem3  46722  hoidmvlelem4  46723  hoidmvle  46725  hspmbllem2  46752  hoimbl2  46790  vonhoire  46797  vonicclem2  46809  vonn0ioo2  46815  vonn0icc2  46817  salpreimagelt  46832  salpreimalegt  46834  pimdecfgtioc  46840  pimincfltioc  46841  pimincfltioo  46843  salpreimagtge  46850  salpreimaltle  46851  salpreimagtlt  46855  incsmf  46867  decsmf  46892  smflimlem1  46896  smflimlem2  46897  smflimlem3  46898  smflimlem4  46899  smfpimcclem  46932  funressnmo  47173  fcoresf1  47196  aiota0def  47223  euoreqb  47236  2reu8i  47240  2reuimp0  47241  funressndmafv2rn  47350  funressnbrafv2  47371  funbrafv2  47374  smonoord  47498  elsetpreimafvbi  47518  iccpartgt  47554  iccelpart  47560  iccpartiun  47561  icceuelpartlem  47562  icceuelpart  47563  iccpartnel  47565  fargshiftf1  47568  ichexmpl2  47597  ichnreuop  47599  ichreuopeq  47600  sprsymrelfolem2  47620  prproropf1olem4  47633  paireqne  47638  reupr  47649  reuopreuprim  47653  fmtnofac2  47696  fmtnofac1  47697  prmdvdsfmtnof1lem2  47712  perfectALTVlem2  47849  nfermltl8rev  47869  nfermltl2rev  47870  sbgoldbwt  47904  sbgoldbst  47905  sgoldbeven3prm  47910  sbgoldbm  47911  nnsum4primesodd  47923  nnsum4primesoddALTV  47924  evengpop3  47925  evengpoap3  47926  bgoldbnnsum3prm  47931  bgoldbtbndlem4  47935  bgoldbtbnd  47936  tgblthelfgott  47942  tgoldbach  47944  grimuhgr  48014  grimcnv  48015  isuspgrimlem  48022  isubgr3stgrlem4  48096  isubgr3stgrlem6  48098  isubgr3stgrlem7  48099  gpgedg2ov  48193  gpgedg2iv  48194  pgnbgreunbgrlem2lem1  48241  pgnbgreunbgrlem2lem2  48242  pgnbgreunbgrlem2lem3  48243  pgnbgreunbgrlem5lem1  48247  pgnbgreunbgrlem5lem2  48248  pgnbgreunbgrlem5lem3  48249  pgnbgreunbgr  48252  ply1mulgsumlem2  48515  islininds  48574  linindslinci  48576  lindslinindsimp1  48585  linds0  48593  lindsrng01  48596  snlindsntorlem  48598  snlindsntor  48599  ldepsnlinc  48636  nn0sumshdiglemA  48747  nn0sumshdiglemB  48748  nn0sumshdiglem1  48749  nn0sumshdiglem2  48750  nn0sumshdig  48751  itschlc0yqe  48888  f1mo  48980  iscnrm3lem5  49064  iscnrm3r  49075  isprsd  49082  lubeldm2d  49085  glbeldm2d  49086  joindm2  49095  meetdm2  49097  ipolublem  49113  ipolub  49115  ipoglblem  49116  ipoglb  49118  oppcendc  49146  oppcthinendcALT  49569  functhinclem2  49573  fullthinc  49578  fullthinc2  49579  euendfunc  49654  bnd2d  49809  setrec1lem1  49815  setrec1lem4  49818  setrec2fun  49820