Theorem imbi12d 347

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 344	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 343	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	bitrd 282	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12  349  ifpbi123d  1095  nfbiit  1883  nfbidv  1956  sbjust  2099  nfbidf  2263  cbvsbvf  2395  drnf1v  2403  drnf1  2475  mo4  2594  cbvmovw  2630  cbvmow  2631  axextg  2737  rspw  3242  cbvralvw  3243  cbvralfw  3305  raleqbidv  3337  cbvraldva2  3339  sbralie  3341  sbralieOLD  3343  cbvralf  3348  ralcom2  3365  vtoclgaf  3538  vtoclga  3539  rspct  3565  rspc  3567  rspc2gv  3588  rexraleqim  3603  ralab2  3657  nelrdva  3665  mob2  3675  mob  3677  morex  3679  reu7  3692  reu8  3693  reu2eqd  3696  cdeqim  3733  sbcimg  3789  sbcim1  3794  sbceqal  3802  csbhypf  3878  cbvralcsf  3892  dfssf  3903  reldisj  4408  ralidmw  4474  reusngf  4634  rexreusng  4639  reuprg0  4662  elpreqpr  4824  unissb  4903  intss1  4925  intmin  4930  dftr2c  5217  trel  5222  zfpow  5331  reusv2lem4  5366  reusv3i  5369  rext  5419  opth  5448  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  cotsexgw  5466  poeq1  5565  pocl  5570  swopolem  5572  swopo  5573  isso2i  5599  vtoclr  5717  poinxp  5736  posn  5741  ssrel  5763  ssrel2  5765  ssrelrel  5776  relop  5832  cotrg  6110  cnvsym  6113  reu3op  6301  reuop  6302  dfpo2  6305  preddowncl  6341  frpoinsg  6352  ordelord  6390  iota5  6528  dffun2  6556  fununiq  6563  sbcfungOLD  6572  funopg  6582  brprcneu  6883  brprcneuALT  6884  tz6.12f  6918  funbrfv  6941  ssimaexg  6979  fvmptf  7023  fvelrn  7084  fprg  7167  dff13f  7266  f1veqaeq  7267  fpropnf1  7278  f1ounsn  7287  nf1const  7319  soisores  7342  soisoi  7343  isofrlem  7355  isopolem  7360  weniso  7371  riota5f  7412  imbrov2fvoveq  7452  oprabidw  7458  oprabid  7459  f1opr  7483  ovmpos  7575  ov2gf  7576  ov3  7590  caovcan  7632  caovordig  7633  caofrss  7739  caoftrn  7741  tfisg  7872  tfis  7873  tfisi  7877  tfindsg  7879  tfindsg2  7880  tfindes  7881  dfom2  7886  limomss  7889  nnlim  7898  peano5  7912  findsg  7916  findes  7919  resf1extb  7953  f1oweALT  7991  dfoprab4f  8075  offval22  8107  f1o2ndf1  8143  frxp  8148  poxp  8150  fnwe2lem3  8157  frpoins3xpg  8167  frpoins3xp3g  8168  poxp2  8170  frxp2  8171  xpord2indlem  8174  poxp3  8177  frxp3  8178  xpord3inddlem  8181  suppfnss  8217  onfununi  8360  smoel  8379  smogt  8386  tfrlem1  8394  onelfvnef1  8460  tz7.48lemOLD  8462  tz7.49  8466  oawordeu  8574  omordi  8585  oeordi  8607  nnmordi  8651  omabs  8671  nneob  8676  omsmolem  8677  qsel  8828  eroveu  8844  ecopovtrn  8852  ixpsnf1o  8977  funen1cnv  9067  fundmeng  9071  sbth  9127  limensuc  9184  findcard  9190  findcard2  9191  findcard2d  9193  pssnn  9195  ssfi  9199  sbthfi  9225  nneneq  9232  php  9233  unxpdom  9261  findcard3  9285  ac6sfi  9286  frfi  9287  domunfican  9324  fiint  9329  iunfi  9343  finsschain  9359  dffi3  9433  marypha1lem  9435  marypha1  9436  supeq3  9451  supeq123d  9452  supmo  9454  suplub  9462  supisolem  9476  eqinf  9487  infval  9489  infmo  9499  ordiso2  9519  ordtypelem7  9528  wemaplem1  9550  wemaplem2  9551  zfregcl  9598  zfregclOLD  9599  elirrv  9601  elirrvOLD  9602  inf0  9632  inf3lem1  9639  zfinf  9650  axinf2  9651  dfom3  9658  elom3  9659  cantnfval2  9680  cantnfle  9682  cantnflt  9683  cantnfp1lem3  9691  oemapvali  9695  cantnflem1c  9698  cantnflem1  9700  cantnf  9704  wemapwe  9708  cnfcom  9711  ttrclss  9731  ttrclselem2  9737  setind  9758  setinds  9760  frmin  9763  frinsg  9765  r1sdom  9791  r1ordg  9795  rankonidlem  9848  rankelg  9862  rankunb  9874  r1filimi  9913  scottabf  9949  bnd2  9966  setrec1lem1  9976  bnd2d  9978  setrec1lem4  9981  setrec2fun  9983  infxpenlem  10102  infxpenc2  10111  dfac8alem  10118  dfac8clem  10121  indcardi  10130  alephordi  10163  alephinit  10184  alephfp  10197  aceq3lem  10209  dfac5lem4  10215  dfac5  10217  dfac2b  10219  dfac9  10225  dfac12lem2  10233  dfac12lem3  10234  kmlem1  10239  kmlem4  10242  kmlem10  10248  kmlem12  10250  kmlem13  10251  pwsdompw  10291  ackbij1lem16  10322  cfslb2n  10356  cfsmolem  10358  sornom  10365  fin2i  10383  infpssrlem4  10394  isfin2-2  10407  isfin3ds  10417  fin23lem17  10426  fin23lem32  10432  fin23lem34  10434  fin23lem35  10435  fin23lem39  10438  fin23lem41  10440  isf32lem2  10442  isf33lem  10454  isf34lem4  10465  isf34lem6  10468  fin1a2lem10  10497  axcc2lem  10524  axcc3  10526  axcc4dom  10529  dominf  10533  axdc2lem  10536  axdc3lem2  10539  ac6sg  10576  zorn2lem7  10590  zornn0g  10593  ttukeylem5  10601  ttukeylem6  10602  axdclem  10607  dominfac  10668  axrepndlem1  10687  axrepndlem2  10688  axunndlem1  10690  axunnd  10691  axpowndlem2  10693  axpowndlem3  10694  axpowndlem4  10695  axregndlem2  10698  axregnd  10699  axinfndlem1  10700  axinfnd  10701  axacndlem4  10705  axacndlem5  10706  axacnd  10707  zfcndpow  10711  zfcndinf  10713  fpwwe2lem4  10729  fpwwe2lem7  10732  fpwwe2lem11  10736  pwfseqlem4a  10756  pwfseqlem4  10757  pwfseqlem5  10758  pwfseq  10759  wunfi  10816  wunex2  10833  inar1  10870  rankcf  10872  tskord  10875  grudomon  10912  grur1a  10914  axgroth6  10923  axgroth3  10926  axgroth4  10927  eltskm  10938  indpi  11002  pinq  11022  nqereu  11024  prcdnq  11088  prnmax  11090  ltsopr  11127  prlem936  11142  ltsosr  11189  recexsrlem  11198  mulgt0sr  11200  map2psrpr  11205  supsrlem  11206  axrrecex  11258  axpre-lttrn  11261  axpre-mulgt0  11263  axpre-sup  11264  axsup  11395  dedekind  11483  ltordlem  11851  ltord1  11852  wloglei  11858  squeeze0  12230  infm3  12286  nnsub  12392  nnunb  12612  peano5uzti  12799  fzind  12807  uzind4s  13045  uzind4s2  13046  zmax  13082  zbtwnre  13083  xmulasslem  13425  xrsupsslem  13447  xrinfmsslem  13448  xrub  13452  infmremnf  13484  injresinj  13936  f1resfz0f1d  13937  om2uzlti  14103  uzindi  14135  axdc4uz  14137  ssnn0fi  14138  rabssnn0fi  14139  suppssfz  14147  seqp1  14169  seqcl2  14173  seqfveq2  14177  seqshft2  14181  monoord  14185  seqsplit  14188  seqf1olem2  14195  seqf1o  14196  seqid2  14201  seqhomo  14202  seqof2  14213  expcl2lem  14226  facdiv  14441  facwordi  14443  faclbnd4lem2  14448  hashnn0n0nn  14545  hashf1lem2  14611  seqcoll  14619  fi1uzind  14662  brfi1indALT  14665  wrdind  14882  wrd2ind  14883  swrdccatin1  14885  swrdccat3blem  14899  reuccatpfxs1lem  14906  repswccat  14948  cshf1  14972  trclfvcotr  15174  relexprelg  15203  rtrclreclem4  15226  relexpindlem  15228  ello1mpt  15700  o1co  15765  o1compt  15766  rlimcn3  15769  climcn2  15772  subcn2  15774  o1of2  15792  fsumclf  15916  fsumsplitf  15920  fsumsplit1  15923  fsum2d  15949  modfsummod  15973  fsumabs  15980  telfsumo  15981  fsumrlim  15990  fsumo1  15991  o1fsum  15992  fsumiun  16000  prodfdiv  16077  fprod2d  16160  fproddivf  16166  fprodsplitf  16167  fprodsplit1f  16169  rpnnen2lem10  16403  sqrt2irr  16429  dvdsle  16492  divalglem7  16581  divalglem8  16582  ndvdssub  16591  gcdcllem1  16681  dfgcd2  16731  algcvg  16763  algcvga  16766  algfx  16767  lcmgcdlem  16793  lcmdvds  16795  lcmf  16820  lcmfunsnlem1  16824  lcmfunsnlem2lem1  16825  lcmfunsnlem  16828  lcmfdvds  16829  lcmfun  16832  coprmgcdb  16836  coprmdvds1  16839  coprmdvds2  16841  coprmprod  16848  coprmproddvds  16850  prmind2  16872  dvdsprime  16874  nprm  16875  dvdsprm  16891  exprmfct  16892  coprm  16899  isprm6  16902  prmfac1  16908  eulerthlem2  16971  pcqmul  17043  pcqcl  17046  pc2dvds  17069  pcz  17071  prmpwdvds  17094  infpn2  17103  vdwlem12  17182  ramub2  17204  rami  17205  ramcl  17219  prmdvdsprmop  17233  prmlem0  17295  mreintcl  17777  ismred2  17785  mrissmrcd  17826  mreexexlemd  17830  iscatd2  17867  moni  17923  yoniso  18471  isprs  18482  prslem  18483  drsdirfi  18491  ispos  18500  posi  18503  isposd  18508  pospropd  18511  lubfval  18534  lublecllem  18544  glbfval  18547  joinle  18570  meetle  18584  poslubmo  18595  posglbmo  18596  resspos  18615  lubl  18698  lubun  18701  clatleglb  18704  ipodrsima  18727  acsdrsel  18729  isacs4lem  18730  isacs5lem  18731  acsdrscl  18732  mreclatBAD  18749  pslem  18758  dirtr  18788  chnind  18807  mndind  19036  degenmgm2nfun  19151  mhmlem  19284  isnsg2  19378  ghmf1  19472  orbsta  19539  symgextf1  19647  gsmsymgrfix  19654  gsmsymgreq  19658  symggen  19696  psgnunilem4  19723  sylow1lem1  19824  sylow2alem2  19844  sylow2a  19845  lsmmod  19901  lsmdisj2  19908  efgsrel  19960  efgredlemd  19970  efgredlem  19973  efgred  19974  gsumzaddlem  20147  gsummptnn0fz  20212  gsummptnn0fzfv  20213  telgsumfzs  20215  telgsums  20219  dprdval  20231  dprddisj2  20267  ablfac1eulem  20300  pgpfac1lem1  20302  pgpfac1lem5  20307  pgpfac1  20308  pgpfaclem2  20310  pgpfac  20312  isomnd  20349  omndadd  20354  gsumle  20371  irredmul  20671  islring  20804  lringuplu  20808  rrgval  20961  rrgeq0i  20963  isdomn  20969  domneq0  20972  isdomn4  20979  domnlcanb  20983  domnrcanb  20985  isdrngrd  21035  isdrngrdOLD  21037  sdrgacs  21070  isorng  21130  orngmul  21134  islbs3  21445  rngqiprngimf1lem  21602  isprmidl  21631  prmidl  21633  prmidlc  21641  prmidlprop  21644  ssdifidlprm  21654  cnsubrglem  21735  prmirredlem  21790  znfld  21878  znrrg  21883  cygznlem3  21887  isphl  21946  ipeq0  21956  isphld  21972  phlpropd  21973  lsmcss  22010  frlmphl  22099  frlmup1  22116  lindfrn  22139  islindf4  22156  islindf5  22157  mplsubglem  22318  mpllsslem  22319  mplcoe1  22358  mplcoe5  22361  mpfind  22436  ismhp3  22475  coe1fzgsumd  22634  gsummoncoe1  22638  pf1ind  22685  evl1gsumd  22687  dmatelnd  22823  mat1scmat  22866  mdetdiaglem  22925  mdetralt  22935  mdetralt2  22936  mdetunilem1  22939  mdetunilem2  22940  mdetunilem3  22941  mdetunilem4  22942  mdetunilem9  22947  smadiadetr  23002  matunitlindflem1  23006  pmatcoe1fsupp  23031  mp2pm2mplem4  23139  uniopn  23227  fiinopn  23231  epttop  23339  clsndisj  23405  elcls3  23413  neiptoptop  23461  neiptopnei  23462  cnpval  23566  iscnp  23567  cnpimaex  23586  lmcvg  23592  cnprest  23619  cnprest2  23620  lmss  23628  lmff  23631  t0sep  23654  hausnei  23658  isnrm2  23688  t1sep2  23699  isreg2  23707  iscmp  23718  cmpcov  23719  cmpsublem  23729  cmpsub  23730  tgcmp  23731  uncmp  23733  fiuncmp  23734  hauscmplem  23736  cmpfi  23738  cmpfii  23739  dfconn2  23749  connsuba  23750  connsub  23751  nconnsubb  23753  1stcclb  23774  1stcfb  23775  2ndc1stc  23781  1stcrest  23783  1stcelcls  23792  restnlly  23813  lly1stc  23827  comppfsc  23863  kgenval  23866  kgeni  23868  kgencn2  23888  ptcldmpt  23945  ptclsg  23946  dfac14lem  23948  dfac14  23949  txcnp  23951  ptcnp  23953  hausdiag  23976  txlm  23979  tx1stc  23981  xkococn  23991  cnmpt12  23998  cnmpt22  24005  kqt0lem  24067  isr0  24068  regr1lem2  24071  kqreglem1  24072  r0sep  24079  ptcmpfi  24144  elmptrab  24158  isfil  24178  filss  24184  isufil2  24239  cfinufil  24259  rnelfm  24284  fmfnfmlem2  24286  fmfnfmlem4  24288  flimopn  24306  flimrest  24314  flftg  24327  cnpflf  24332  txflf  24337  fclsopni  24346  fclsrest  24355  fclscf  24356  flimfnfcls  24359  fcfnei  24366  alexsublem  24375  alexsubb  24377  alexsubALTlem3  24380  alexsubALTlem4  24381  alexsubALT  24382  cnextcn  24398  cnextfres1  24399  tgpt0  24450  qustgplem  24452  tsmsi  24465  tsmssubm  24474  tsmsres  24475  tsmsf1o  24476  tsmsxp  24486  ustssel  24537  ust0  24551  ustuqtop4  24575  ucnima  24611  ucncn  24615  iscusp  24629  cuspcvg  24631  imasdsf1olem  24704  blssps  24755  blss  24756  metss  24839  comet  24844  metcnp3  24871  metcnp2  24873  txmetcnp  24878  metuel2  24896  metucn  24902  nrmmetd  24905  nlmvscn  25018  nrginvrcn  25023  nmolb  25048  xrge0tsms  25166  mpomulcn  25200  divcn  25201  fsumcn  25203  elcncf2  25223  cncfi  25227  mulc1cncf  25238  cncfmet  25242  xrhmeo  25279  bndth  25291  nmoleub2lem2  25449  nmoleub3  25452  ipcn  25579  lmmbr  25591  caucfil  25616  pmltpc  25783  ovolfiniun  25834  ovolicc2lem3  25852  ovolicc2  25855  mblsplit  25865  finiunmbl  25877  volfiniun  25880  voliunlem3  25885  ioorinv  25909  ioorcl  25910  dyadmax  25931  dyadmbllem  25932  dyadmbl  25933  opnmbllem  25934  volcn  25939  vitalilem2  25942  vitalilem3  25943  vitali  25946  i1fd  26014  itg2seq  26075  itg2addlem  26091  itgfsum  26159  ellimc3  26211  dvbsss  26234  dvnres  26263  dvmptfsum  26307  dvferm1lem  26316  dvferm2lem  26318  rolle  26322  c1lip1  26329  lhop1lem  26345  lhop1  26346  dvfsumlem2  26359  dvfsumlem4  26361  dvfsumrlim  26363  dvfsum2  26366  ftc1a  26369  ftc1lem6  26373  mdegleb  26394  mdeglt  26395  deg1leb  26425  deg1lt  26427  ply1divex  26467  fta1glem2  26499  fta1g  26500  plyco0  26522  plyeq0lem  26541  coeeq2  26573  dgrle  26574  dgrcolem2  26605  dgrco  26606  plydivlem4  26629  plydivex  26630  fta1lem  26640  fta1  26641  vieta1lem2  26646  vieta1  26647  aalioulem2  26672  aalioulem4  26674  abelth  26780  cxpcn3  27088  rlimcnp  27305  xrlimcnp  27308  cxploglim  27317  scvxcvx  27325  jensen  27328  lgamgulmlem2  27369  wilthlem2  27408  wilthlem3  27409  fta  27419  mpodvdsmulf1o  27533  dvdsmulf1o  27535  perfectlem2  27569  dchrelbas3  27577  dchrelbas4  27582  dchrn0  27589  bcmono  27616  lgsdir2lem4  27667  lgsdchr  27694  gausslemma2dlem0i  27703  lgseisenlem2  27715  lgsquad2lem2  27724  2sqlem6  27762  2sqlem8  27765  2sqlem10  27767  dchrisumlema  27827  dchrisumlem2  27829  dchrisumlem3  27830  fltoprmlem2  28006  fltoprm  28007  nosupprefixmo  28069  noinfprefixmo  28070  nosupcbv  28071  nosupdm  28073  nosupfv  28075  nosupres  28076  nosupbnd1lem1  28077  nosupbnd1lem3  28079  nosupbnd1lem5  28081  nosupbnd2  28085  noinfcbv  28086  noinfdm  28088  noinffv  28090  noinfres  28091  noinfbnd1lem1  28092  noinfbnd1lem3  28094  noinfbnd1lem5  28096  noinfbnd2  28100  nocvxminlem  28152  madebdaylemold  28296  madebdaylemlrcut  28297  madebday  28298  lrrecpo  28339  addsproplem1  28367  addsprop  28374  leadds1  28387  negsproplem1  28426  negsprop  28433  mulsproplemcbv  28513  mulsproplem1  28514  mulsprop  28528  precsexlem8  28612  precsexlem9  28613  precsexlem11  28615  precsex  28616  bdayons  28674  addonbday  28677  onsfi  28754  n0subs  28761  oldfib  28775  eln0zs  28798  bdaypw2n0bndlem  28861  bdaypw2n0bnd  28862  bdayfinbndcbv  28864  bdayfinbndlem1  28865  bdayfinbndlem2  28866  bdayfinbnd  28867  istrkgb  28929  istrkgcb  28930  istrkge  28931  axtgcgrid  28937  axtg5seg  28939  axtgbtwnid  28940  axtgpasch  28941  axtgcont1  28942  axtgeucl  28946  iscgrglt  28989  tgcgr4  29006  axcgrtr  29505  gropd  29621  grstructd  29622  upgredg2vtx  29731  upgredgpr  29732  edglnl  29733  numedglnl  29734  usgredg2vtxeuALT  29815  nbgr2vtx1edg  29943  finsumvtxdg2size  30143  wlkp1lem8  30271  upgrwlkdvdelem  30334  usgr2wlkneq  30354  usgr2pthlem  30361  pthdlem2lem  30365  uspgrn2crct  30409  2pthdlem1  30531  eleclclwwlkn  30679  hashecclwwlkn1  30680  umgrhashecclwwlk  30681  acycgrcycl  30765  3pthdlem1  30777  eupth2  30852  frgr3vlem1  30886  3vfriswmgrlem  30890  frgrwopreglem4a  30923  frgr2wwlk1  30942  wlkl0  30980  numclwlk2lem2f1o  30992  friendshipgt3  31011  eulplig  31099  nvz  31283  nmobndseqi  31393  nmobndseqiALT  31394  nmlno0  31409  blocnilem  31418  dipdir  31456  dipass  31459  siilem2  31466  ubthlem2  31485  ubth  31487  htth  31532  normpyth  31759  norm3lemt  31766  chlimi  31848  chcompl  31856  omlsii  32017  pjoml  32050  h1de2i  32167  elspansn2  32181  h1datom  32196  pjoml2  32225  pjoml3  32226  lecm  32231  chscllem2  32252  osum  32259  spansncv  32267  pjcjt2  32306  pjopyth  32334  eigre  32449  eigorth  32452  hhcno  32518  hhcnf  32519  cnopc  32527  cnfnc  32544  nmcexi  32640  nmcopexi  32641  nmcfnexi  32665  pjssge0i  32780  hstel2  32833  stj  32849  stri  32871  hstri  32879  stcltr1i  32888  mdbr  32908  mdi  32909  mdbr3  32911  mdbr4  32912  dmdbr  32913  dmdmd  32914  dmdi  32916  dmdbr3  32919  dmdbr4  32920  dmdbr5  32922  mdsl1i  32935  mdslmd1lem3  32941  mdslmd1lem4  32942  mdslmd1i  32943  csmdsymi  32948  cvmd  32950  atss  32960  atom1d  32967  chcv1  32969  hatomic  32974  atord  33002  atcvat2  33003  mddmdin0i  33045  opreu2reuALT  33127  rmoxfrd  33143  ifeqeqx  33192  ssiun2sf  33208  iinabrex  33217  ssrelf  33263  fmptcof2  33305  acunirnmpt  33307  aciunf1lem  33310  suppovss  33328  fz1nntr  33447  nn0min  33465  fsumiunle  33473  wrdt2ind  33569  ressprs  33580  toslublem  33586  tosglblem  33588  mntoval  33596  ismntd  33598  dfmgc2lem  33609  dfmgc2  33610  xrge0tsmsd  33687  fzto1st  33717  psgnfzto1st  33719  submarchi  33800  archirng  33802  archiexdiv  33804  archiabllem1a  33805  archiabllem2a  33808  archiabl  33812  isarchiofld  33813  gsumvsca1  33840  gsumvsca2  33841  elrgspnlem4  33859  domnpropd  33894  linds2eq  33989  ismxidl  34040  mxidlmax  34043  rprmval  34101  isrprm  34102  rprmdvds  34104  rprmdvdsprod  34119  1arithidomlem1  34120  1arithidom  34122  1arithufdlem3  34131  dfufd2lem  34134  lbsdiflsp0  34311  fedgmullem1  34314  fedgmullem2  34315  fldext2chn  34413  constrmon  34429  submateq  34494  lmatfval  34499  lmatcl  34501  iscref  34529  crefi  34532  pcmplfin  34545  xrge0iifiso  34620  esumcvg  34771  esum2dlem  34777  sigaclcu  34802  sigaclci  34817  unelsiga  34819  unelldsys  34844  sigapildsys  34848  ldgenpisyslem1  34849  fiunelros  34860  measvun  34895  measiun  34904  carsgmon  34999  carsgsigalem  35000  carsgclctunlem2  35004  carsgclctun  35006  pmeasmono  35009  pmeasadd  35010  sibfof  35025  sitgclg  35027  eulerpartlemgvv  35061  signsply0  35233  signstfvneq0  35254  breprexp  35315  hgt749d  35331  istrkg2d  35348  axtgupdim2ALTV  35350  bnj1385  35515  bnj110  35541  bnj222  35566  bnj229  35567  bnj590  35593  bnj865  35606  bnj849  35608  bnj981  35633  bnj1014  35644  bnj1015  35645  bnj1112  35666  bnj1118  35667  bnj1123  35669  bnj1128  35673  bnj1125  35675  bnj1148  35679  bnj1154  35682  bnj1326  35709  bnj1384  35715  bnj1489  35739  bnj1497  35743  trssfir1om  35798  r1omhfb  35799  setindregs  35869  trssfir1omregs  35875  r1omhfbregs  35876  axpowg  35885  onvf1odlem2  35986  cplgredgex  36016  srepdf  36041  subfacp1lem6  36071  erdszelem9  36085  kur14lem9  36100  sconnpht  36115  cvmsss2  36160  cvmliftlem7  36177  cvmliftlem10  36180  fmlasuc  36272  gonar  36281  goalr  36283  mclsrcl  36447  mclsssvlem  36448  mclsval  36449  mclsax  36455  mclsind  36456  mclsppslem  36469  iota5f  36616  dfon2lem3  36674  dfon2lem4  36675  dfon2lem5  36676  dfon2lem6  36677  dfon2lem7  36678  dfon2lem8  36679  dfon2  36681  btwnconn1lem11  36989  linethru  37045  fwddifnp1  37057  rankeq1o  37059  sbequbidv  37130  cbvralvw2  37142  cbvmodavw  37166  cbvsbdavw  37170  cbvsbdavw2  37171  subtr  37229  subtr2  37230  trer  37231  nn0prpwlem  37237  nn0prpw  37238  neibastop2lem  37275  filnetlem4  37296  axtco1from2  37390  axtcond  37393  axuntco  37394  dfttc4lem2  37444  dfttc4  37445  mh-setindnd  37452  regsfromregtco  37453  regsfromsetind  37454  mh-unprimbi  37459  mh-infprim2bi  37462  bj-hbxfrbi  37639  bj-hbyfrbi  37640  bj-ssblem1  37680  bj-ssblem2  37681  bj-ax12  37683  irrdiff  38387  relowlssretop  38426  rdgeqoa  38433  rdgssun  38441  exrecfnlem  38442  finxpreclem6  38459  pibp19  38477  pibt2  38480  wl-ax12v2cl  38569  wl-mo3t  38648  wl-sb8mot  38652  wl-sb8motv  38653  finixpnum  38668  ptrest  38677  poimirlem13  38691  poimirlem14  38692  poimirlem17  38695  poimirlem18  38696  poimirlem20  38698  poimirlem21  38699  poimirlem22  38700  poimirlem24  38702  poimirlem25  38703  poimirlem26  38704  poimirlem28  38706  poimirlem30  38708  poimirlem31  38709  poimirlem32  38710  poimir  38711  heicant  38713  mblfinlem1  38715  mblfinlem2  38716  mblfinlem3  38717  voliunnfl  38722  volsupnfl  38723  mbfresfi  38724  itg2addnclem3  38731  ftc1cnnc  38750  ftc1anclem7  38757  ftc1anc  38759  findcard4  38772  sdclem2  38816  fdc  38819  fdc1  38820  neificl  38827  mettrifi  38831  sstotbnd2  38848  cntotbnd  38870  heibor1lem  38883  bfp  38898  isass  38920  ismgmOLD  38924  isexid2  38929  iscringd  39072  ispridl  39108  pridl  39111  ismaxidl  39114  maxidlmax  39117  ispridlc  39144  pridlc  39145  dmnnzd  39149  relcnveq2  39401  ecin0  39424  elrelscnveq2  39701  elsymrels3  39710  eltrrels3  39736  eleqvrels3  39749  eqvrelqsel  39772  disjimeceqim2  39877  eldisjim3  39887  eldisjlem19  39985  eldisjsim3  40009  axc11n-16  40135  ax12eq  40138  ax12el  40139  ax12inda  40145  ax12v2-o  40146  fsumshftd  40149  riotasv2d  40154  lshpdisj  40184  lsmsatcv  40207  lsat0cv  40230  lcvexchlem4  40234  lcvexchlem5  40235  l1cvpat  40251  isopos  40377  oposlem  40379  isoml  40435  omllaw  40440  isatl  40496  atlex  40513  iscvlat  40520  cvlexch1  40525  glbconN  40574  hlsuprexch  40578  ps-1  40674  3atlem5  40684  psubspi  40944  llnexchb2  41066  elpcliN  41090  pclfinclN  41147  ldilval  41310  ltrnfset  41314  ltrnset  41315  ltrnu  41318  trlfset  41357  trlset  41358  trlval2  41360  cdleme25cv  41555  cdleme31so  41576  cdleme31fv  41587  cdlemefrs29bpre0  41593  cdleme32fva  41634  cdleme40v  41666  trlord  41766  cdlemkid3N  42130  cdlemkid4  42131  dihffval  42427  dihfval  42428  dihval  42429  lpolconN  42684  mapdordlem2  42834  hdmapfval  43024  hdmapval  43025  hdmapval2  43029  aks4d1p7  43273  isprimroot  43283  primrootlekpowne0  43295  sticksstones1  43336  sticksstones2  43337  sticksstones10  43345  sticksstones12a  43347  aks6d1c6lem3  43362  indstrd  43383  unitscyglem2  43386  unitscyglem3  43387  unitscyglem4  43388  nnn1suc  43471  fsuppind  43758  eu6w  43827  ismrcd1  43849  ismrcd2  43850  ismrc  43852  isnacs3  43861  nacsfix  43863  mzpcompact2  43903  fphpd  43963  fphpdo  43964  monotuz  44088  monotoddzzfi  44089  monotoddzz  44090  oddcomabszz  44091  zindbi  44093  setindtrs  44172  dford3lem2  44174  ttac  44183  dnnumch1  44191  aomclem3  44198  aomclem6  44201  aomclem8  44203  dfac11  44204  dfac21  44208  islssfg2  44213  hbtlem5  44270  hbt  44272  flcidc  44312  mendlmod  44331  unielss  44360  rababg  44715  elmapintrab  44717  iunrelexpuztr  44859  frege92  45095  frege104  45107  ntrkbimka  45178  ntrk0kbimka  45179  neik0pk1imk0  45187  isotone1  45188  isotone2  45189  ntrclsiso  45207  ntrclskb  45209  ntrneiiso  45231  ntrneik3  45236  ntrneix3  45237  gneispacess2  45286  grur1cld  45370  ismnu  45385  mnuop23d  45390  mnuunid  45401  ismnushort  45425  dvgrat  45436  cvgdvgrat  45437  binomcxplemnotnn0  45480  pm14.122b  45546  sbiota1  45557  relprel  46080  relpfrlem  46082  modelaxreplem1  46107  modelaxreplem2  46108  modelaxrep  46110  omssaxinf2  46117  modelac8prim  46121  permaxinf2lem  46141  permac8prim  46143  nregmodel  46146  fnchoice  46185  fiiuncl  46221  iunincfi  46248  disjf1  46337  wessf1ornlem  46339  disjinfi  46346  axccdom  46374  dmrelrnrel  46378  axccd  46380  monoords  46452  fperiodmullem  46458  supxrgere  46484  supxrgelem  46488  supxrge  46489  xrlexaddrp  46503  infxr  46517  infleinf  46522  supxrleubrnmptf  46600  monoordxrv  46630  monoordxr  46631  monoord2xr  46633  fsummulc1f  46722  fsumnncl  46723  fsumf1of  46725  fsumreclf  46727  fsumlessf  46728  fsumsermpt  46730  fmul01  46731  fmulcl  46732  fmuldfeqlem1  46733  fmuldfeq  46734  fmul01lt1lem1  46735  fmul01lt1lem2  46736  fprodexp  46745  fprodabs2  46746  fprodcnlem  46750  climmulf  46755  climexp  46756  climsuse  46759  climrecf  46760  climinff  46762  climaddf  46766  mullimc  46767  mullimcf  46774  limcperiod  46779  sumnnodd  46781  lptre2pt  46789  limsupre  46790  neglimc  46796  addlimc  46797  0ellimcdiv  46798  limclner  46800  climsubmpt  46809  climreclf  46813  climeldmeqmpt  46817  climfveqmpt  46820  fnlimfvre  46823  climfveqf  46829  climfveqmpt3  46831  climeldmeqf  46832  limsupref  46834  limsupbnd1f  46835  climeqf  46837  climeldmeqmpt3  46838  climinf2  46856  limsupubuz  46862  climinf2mpt  46863  climinfmpt  46864  limsupmnf  46870  limsupequz  46872  limsupre2  46874  limsupequzmptf  46880  limsupre3  46882  lmbr3  46896  cnrefiisp  46979  xlimxrre  46980  xlimmnfvlem1  46981  xlimpnfvlem1  46985  climxlim2lem  46994  cncfshift  47023  cncfperiod  47028  icccncfext  47036  fprodcncf  47049  fperdvper  47068  dvmptmulf  47086  dvnmptdivc  47087  dvnmul  47092  dvmptfprod  47094  dvnprodlem1  47095  dvnprodlem2  47096  dvnprodlem3  47097  iblspltprt  47122  itgspltprt  47128  stoweidlem3  47152  stoweidlem4  47153  stoweidlem6  47155  stoweidlem8  47157  stoweidlem15  47164  stoweidlem16  47165  stoweidlem17  47166  stoweidlem19  47168  stoweidlem20  47169  stoweidlem22  47171  stoweidlem23  47172  stoweidlem26  47175  stoweidlem27  47176  stoweidlem30  47179  stoweidlem31  47180  stoweidlem32  47181  stoweidlem34  47183  stoweidlem35  47184  stoweidlem42  47191  stoweidlem43  47192  stoweidlem48  47197  stoweidlem50  47199  stoweidlem51  47200  stoweidlem57  47206  stoweidlem59  47208  stoweidlem62  47211  wallispilem3  47216  dirkercncflem2  47253  fourierdlem11  47267  fourierdlem12  47268  fourierdlem15  47271  fourierdlem16  47272  fourierdlem21  47277  fourierdlem34  47290  fourierdlem41  47297  fourierdlem42  47298  fourierdlem46  47301  fourierdlem48  47303  fourierdlem49  47304  fourierdlem50  47305  fourierdlem51  47306  fourierdlem68  47323  fourierdlem71  47326  fourierdlem72  47327  fourierdlem73  47328  fourierdlem76  47331  fourierdlem79  47334  fourierdlem81  47336  fourierdlem83  47338  fourierdlem86  47341  fourierdlem89  47344  fourierdlem90  47345  fourierdlem91  47346  fourierdlem92  47347  fourierdlem94  47349  fourierdlem97  47352  fourierdlem103  47358  fourierdlem104  47359  fourierdlem111  47366  fourierdlem112  47367  fourierdlem113  47368  etransclem2  47385  etransclem46  47429  salunicl  47465  saluncl  47466  intsaluni  47478  dfsalgen2  47490  sge0f1o  47531  sge0lempt  47559  sge0iunmptlemfi  47562  sge0p1  47563  sge0fodjrnlem  47565  sge0iunmpt  47567  sge0ltfirpmpt2  47575  sge0isummpt2  47581  sge0xaddlem2  47583  sge0xadd  47584  nnfoctbdjlem  47604  meadjuni  47606  meadjiun  47615  voliunsge0lem  47621  meaiuninclem  47629  meaiunincf  47632  meaiuninc3v  47633  meaiuninc3  47634  meaiininclem  47635  meaiininc  47636  omeunile  47654  isomenndlem  47679  ovn0lem  47714  ovnsubaddlem1  47719  hoidmvlelem2  47745  hoidmvlelem3  47746  hoidmvlelem4  47747  hoidmvle  47749  hspmbllem2  47776  hoimbl2  47814  vonhoire  47821  vonicclem2  47833  vonn0ioo2  47839  vonn0icc2  47841  salpreimagelt  47856  salpreimalegt  47858  pimdecfgtioc  47864  pimincfltioc  47865  pimincfltioo  47867  salpreimagtge  47874  salpreimaltle  47875  salpreimagtlt  47879  incsmf  47891  decsmf  47916  smflimlem1  47920  smflimlem2  47921  smflimlem3  47922  smflimlem4  47923  smfpimcclem  47956  funressnmo  48255  fcoresf1  48278  aiota0def  48305  euoreqb  48319  2reu8i  48323  2reuimp0  48324  funressndmafv2rn  48432  funressnbrafv2  48453  funbrafv2  48456  smonoord  48586  elsetpreimafvbi  48612  iccpartgt  48648  iccelpart  48654  iccpartiun  48655  icceuelpartlem  48656  icceuelpart  48657  iccpartnel  48659  fargshiftf1  48662  ichexmpl2  48691  ichnreuop  48693  ichreuopeq  48694  sprsymrelfolem2  48714  prproropf1olem4  48727  paireqne  48732  reupr  48743  reuopreuprim  48747  fmtnofac2  48793  fmtnofac1  48794  prmdvdsfmtnof1lem2  48809  perfectALTVlem2  48959  nfermltl8rev  48979  nfermltl2rev  48980  sbgoldbwt  49014  sbgoldbst  49015  sgoldbeven3prm  49020  sbgoldbm  49021  nnsum4primesodd  49033  nnsum4primesoddALTV  49034  evengpop3  49035  evengpoap3  49036  bgoldbnnsum3prm  49041  bgoldbtbndlem4  49045  bgoldbtbnd  49046  tgblthelfgott  49052  tgoldbach  49054  grimuhgr  49124  grimcnv  49125  isuspgrimlem  49132  isubgr3stgrlem4  49206  isubgr3stgrlem6  49208  isubgr3stgrlem7  49209  gpgedg2ov  49303  gpgedg2iv  49304  pgnbgreunbgrlem2lem1  49351  pgnbgreunbgrlem2lem2  49352  pgnbgreunbgrlem2lem3  49353  pgnbgreunbgrlem5lem1  49357  pgnbgreunbgrlem5lem2  49358  pgnbgreunbgrlem5lem3  49359  pgnbgreunbgr  49362  idomnzd  49582  ply1mulgsumlem2  49638  islininds  49697  linindslinci  49699  lindslinindsimp1  49708  linds0  49716  lindsrng01  49719  snlindsntorlem  49721  snlindsntor  49722  ldepsnlinc  49759  nn0sumshdiglemA  49870  nn0sumshdiglemB  49871  nn0sumshdiglem1  49872  nn0sumshdiglem2  49873  nn0sumshdig  49874  itschlc0yqe  50011  f1mo  50103  iscnrm3lem5  50190  iscnrm3r  50201  isprsd  50208  lubeldm2d  50211  glbeldm2d  50212  joindm2  50221  meetdm2  50223  ipolublem  50239  ipolub  50241  ipoglblem  50242  ipoglb  50244  oppcendc  50271  oppcthinendcALT  50715  functhinclem2  50719  fullthinc  50724  fullthinc2  50725  euendfunc  50800  alsbid  51112  cbvals  51115  nellindf  51184