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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbi12  349  ifpbi123d  1093  nfbiit  1878  nfbidv  1949  rename-sb  2096  nfbidf  2266  cbvsbvf  2401  drnf1v  2409  drnf1  2481  mo4  2600  cbvmovw  2636  cbvmow  2637  axextg  2743  rspw  3248  cbvralvw  3249  cbvralfw  3311  raleqbidv  3345  cbvraldva2  3347  sbralie  3349  sbralieOLD  3351  cbvralf  3356  ralcom2  3373  vtoclgaf  3549  vtoclga  3550  rspct  3576  rspc  3578  rspc2gv  3600  rexraleqim  3615  ralab2  3669  nelrdva  3677  mob2  3687  mob  3689  morex  3691  reu7  3704  reu8  3705  reu2eqd  3708  cdeqim  3745  sbcimg  3801  sbcim1  3806  sbceqal  3814  csbhypf  3889  cbvralcsf  3903  dfssf  3936  reldisj  4419  ralidmw  4482  reusngf  4645  rexreusng  4650  reuprg0  4673  elpreqpr  4836  unissb  4910  intss1  4932  intmin  4937  dftr2c  5225  trel  5230  zfpow  5338  reusv2lem4  5373  reusv3i  5376  rext  5430  opth  5459  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  poeq1  5573  pocl  5578  swopolem  5580  swopo  5581  isso2i  5607  vtoclr  5725  poinxp  5743  posn  5748  ssrel  5770  ssrel2  5772  ssrelrel  5783  relop  5837  cotrg  6112  cnvsym  6115  reu3op  6294  reuop  6295  dfpo2  6298  preddowncl  6334  frpoinsg  6345  ordelord  6383  iota5  6520  dffun2  6547  sbcfung  6561  funopg  6571  brprcneu  6872  brprcneuALT  6873  tz6.12f  6907  funbrfv  6930  ssimaexg  6968  fvmptf  7012  fvelrn  7072  fprg  7153  dff13f  7254  f1veqaeq  7255  fpropnf1  7266  f1ounsn  7271  nf1const  7303  soisores  7326  soisoi  7327  isofrlem  7339  isopolem  7344  weniso  7353  riota5f  7396  imbrov2fvoveq  7436  oprabidw  7442  oprabid  7443  f1opr  7467  ovmpos  7559  ov2gf  7560  ov3  7574  caovcan  7615  caovordig  7616  caofrss  7714  caoftrn  7716  tfisg  7849  tfis  7850  tfisi  7854  tfindsg  7856  tfindsg2  7857  tfindes  7858  dfom2  7863  limomss  7866  nnlim  7875  peano5  7889  findsg  7893  findes  7896  resf1extb  7930  f1oweALT  7968  dfoprab4f  8052  offval22  8082  f1o2ndf1  8116  frxp  8121  poxp  8123  frpoins3xpg  8135  frpoins3xp3g  8136  poxp2  8138  frxp2  8139  xpord2indlem  8142  poxp3  8145  frxp3  8146  xpord3inddlem  8149  suppfnss  8184  onfununi  8327  smoel  8346  smogt  8353  tfrlem1  8361  tz7.48lem  8427  tz7.49  8431  oawordeu  8539  omordi  8550  oeordi  8572  nnmordi  8616  omabs  8636  nneob  8641  omsmolem  8642  qsel  8793  eroveu  8809  ecopovtrn  8817  ixpsnf1o  8935  fundmeng  9028  sbth  9084  limensuc  9141  findcard  9147  findcard2  9148  findcard2d  9150  pssnn  9152  ssfi  9156  sbthfi  9182  nneneq  9189  php  9190  unxpdom  9218  findcard3  9242  ac6sfi  9243  frfi  9244  domunfican  9280  fiint  9285  iunfi  9299  finsschain  9315  dffi3  9390  marypha1lem  9392  marypha1  9393  supeq3  9408  supeq123d  9409  supmo  9411  suplub  9419  supisolem  9433  eqinf  9444  infval  9446  infmo  9456  ordiso2  9476  ordtypelem7  9485  wemaplem1  9507  wemaplem2  9508  zfregcl  9555  zfregclOLD  9556  elirrv  9558  elirrvOLD  9559  inf0  9589  inf3lem1  9596  zfinf  9607  axinf2  9608  dfom3  9615  elom3  9616  cantnfval2  9637  cantnfle  9639  cantnflt  9640  cantnfp1lem3  9648  oemapvali  9652  cantnflem1c  9655  cantnflem1  9657  cantnf  9661  wemapwe  9665  cnfcom  9668  ttrclss  9688  ttrclselem2  9694  setind  9715  setinds  9717  frmin  9720  frinsg  9722  r1sdom  9745  r1ordg  9749  rankonidlem  9799  rankunb  9821  scottabf  9865  bnd2  9878  infxpenlem  9996  infxpenc2  10005  dfac8alem  10012  dfac8clem  10015  indcardi  10024  alephordi  10057  alephinit  10078  alephfp  10091  aceq3lem  10103  dfac5lem4  10109  dfac5  10111  dfac2b  10113  dfac9  10119  dfac12lem2  10127  dfac12lem3  10128  kmlem1  10133  kmlem4  10136  kmlem10  10142  kmlem12  10144  kmlem13  10145  pwsdompw  10185  ackbij1lem16  10216  cfslb2n  10251  cfsmolem  10253  sornom  10260  fin2i  10278  infpssrlem4  10289  isfin2-2  10302  isfin3ds  10312  fin23lem17  10321  fin23lem32  10327  fin23lem34  10329  fin23lem35  10330  fin23lem39  10333  fin23lem41  10335  isf32lem2  10337  isf33lem  10349  isf34lem4  10360  isf34lem6  10363  fin1a2lem10  10392  axcc2lem  10419  axcc3  10421  axcc4dom  10424  dominf  10428  axdc2lem  10431  axdc3lem2  10434  ac6sg  10471  zorn2lem7  10485  zornn0g  10488  ttukeylem5  10496  ttukeylem6  10497  axdclem  10502  dominfac  10557  axrepndlem1  10576  axrepndlem2  10577  axunndlem1  10579  axunnd  10580  axpowndlem2  10582  axpowndlem3  10583  axpowndlem4  10584  axregndlem2  10587  axregnd  10588  axinfndlem1  10589  axinfnd  10590  axacndlem4  10594  axacndlem5  10595  axacnd  10596  zfcndpow  10600  zfcndinf  10602  fpwwe2lem4  10618  fpwwe2lem7  10621  fpwwe2lem11  10625  pwfseqlem4a  10645  pwfseqlem4  10646  pwfseqlem5  10647  pwfseq  10648  wunfi  10705  wunex2  10722  inar1  10759  rankcf  10761  tskord  10764  grudomon  10801  grur1a  10803  axgroth6  10812  axgroth3  10815  axgroth4  10816  eltskm  10827  indpi  10891  pinq  10911  nqereu  10913  prcdnq  10977  prnmax  10979  ltsopr  11016  prlem936  11031  ltsosr  11078  recexsrlem  11087  mulgt0sr  11089  map2psrpr  11094  supsrlem  11095  axrrecex  11147  axpre-lttrn  11150  axpre-mulgt0  11152  axpre-sup  11153  axsup  11284  dedekind  11372  ltordlem  11738  ltord1  11739  wloglei  11745  squeeze0  12117  infm3  12173  nnsub  12279  nnunb  12499  peano5uzti  12685  fzind  12693  uzind4s  12931  uzind4s2  12932  zmax  12968  zbtwnre  12969  xmulasslem  13310  xrsupsslem  13332  xrinfmsslem  13333  xrub  13337  infmremnf  13369  injresinj  13819  om2uzlti  13985  uzindi  14017  axdc4uz  14019  ssnn0fi  14020  rabssnn0fi  14021  suppssfz  14029  seqp1  14051  seqcl2  14055  seqfveq2  14059  seqshft2  14063  monoord  14067  seqsplit  14070  seqf1olem2  14077  seqf1o  14078  seqid2  14083  seqhomo  14084  seqof2  14095  expcl2lem  14108  facdiv  14322  facwordi  14324  faclbnd4lem2  14329  hashnn0n0nn  14426  hashf1lem2  14492  seqcoll  14500  fi1uzind  14543  brfi1indALT  14546  wrdind  14758  wrd2ind  14759  swrdccatin1  14761  swrdccat3blem  14775  reuccatpfxs1lem  14782  repswccat  14822  cshf1  14846  trclfvcotr  15045  relexprelg  15074  rtrclreclem4  15097  relexpindlem  15099  ello1mpt  15571  o1co  15636  o1compt  15637  rlimcn3  15640  climcn2  15643  subcn2  15645  o1of2  15663  fsumclf  15788  fsumsplitf  15792  fsumsplit1  15795  fsum2d  15821  modfsummod  15845  fsumabs  15852  telfsumo  15853  fsumrlim  15862  fsumo1  15863  o1fsum  15864  fsumiun  15872  prodfdiv  15949  fprod2d  16034  fproddivf  16040  fprodsplitf  16041  fprodsplit1f  16043  rpnnen2lem10  16278  sqrt2irr  16304  dvdsle  16367  divalglem7  16456  divalglem8  16457  ndvdssub  16466  gcdcllem1  16556  dfgcd2  16603  algcvg  16633  algcvga  16636  algfx  16637  lcmgcdlem  16663  lcmdvds  16665  lcmf  16690  lcmfunsnlem1  16694  lcmfunsnlem2lem1  16695  lcmfunsnlem  16698  lcmfdvds  16699  lcmfun  16702  coprmgcdb  16706  coprmdvds1  16709  coprmdvds2  16711  coprmprod  16718  coprmproddvds  16720  prmind2  16742  dvdsprime  16744  nprm  16745  dvdsprm  16761  exprmfct  16762  coprm  16769  isprm6  16772  prmfac1  16778  eulerthlem2  16840  pcqmul  16912  pcqcl  16915  pc2dvds  16938  pcz  16940  prmpwdvds  16963  infpn2  16972  vdwlem12  17051  ramub2  17073  rami  17074  ramcl  17088  prmdvdsprmop  17102  prmlem0  17164  mreintcl  17646  ismred2  17654  mrissmrcd  17695  mreexexlemd  17699  iscatd2  17736  moni  17792  yoniso  18340  isprs  18351  prslem  18352  drsdirfi  18360  ispos  18369  posi  18372  isposd  18377  pospropd  18380  lubfval  18403  lublecllem  18413  glbfval  18416  joinle  18439  meetle  18453  poslubmo  18464  posglbmo  18465  resspos  18484  lubl  18567  lubun  18570  clatleglb  18573  ipodrsima  18596  acsdrsel  18598  isacs4lem  18599  isacs5lem  18600  acsdrscl  18601  mreclatBAD  18618  pslem  18627  dirtr  18657  chnind  18676  mndind  18886  mhmlem  19127  isnsg2  19221  ghmf1  19315  orbsta  19382  symgextf1  19490  gsmsymgrfix  19497  gsmsymgreq  19501  symggen  19539  psgnunilem4  19566  sylow1lem1  19667  sylow2alem2  19687  sylow2a  19688  lsmmod  19744  lsmdisj2  19751  efgsrel  19803  efgredlemd  19813  efgredlem  19816  efgred  19817  gsumzaddlem  19990  gsummptnn0fz  20055  gsummptnn0fzfv  20056  telgsumfzs  20058  telgsums  20062  dprdval  20074  dprddisj2  20110  ablfac1eulem  20143  pgpfac1lem1  20145  pgpfac1lem5  20150  pgpfac1  20151  pgpfaclem2  20153  pgpfac  20155  isomnd  20192  omndadd  20197  gsumle  20214  irredmul  20510  islring  20624  lringuplu  20628  rrgval  20781  rrgeq0i  20783  isdomn  20789  domneq0  20792  isdomn4  20799  domnlcanb  20803  domnrcanb  20805  isdrngrd  20847  isdrngrdOLD  20849  sdrgacs  20881  isorng  20941  orngmul  20945  islbs3  21256  rngqiprngimf1lem  21404  isprmidl  21433  prmidl  21435  prmidlc  21443  prmidlprop  21444  ssdifidlprm  21454  cnsubrglem  21535  prmirredlem  21590  znfld  21678  znrrg  21683  cygznlem3  21687  isphl  21746  ipeq0  21756  isphld  21772  phlpropd  21773  lsmcss  21810  frlmphl  21899  frlmup1  21916  lindfrn  21939  islindf4  21956  islindf5  21957  mplsubglem  22116  mpllsslem  22117  mplcoe1  22156  mplcoe5  22159  mpfind  22234  ismhp3  22273  coe1fzgsumd  22432  gsummoncoe1  22436  pf1ind  22483  evl1gsumd  22485  dmatelnd  22621  mat1scmat  22664  mdetdiaglem  22723  mdetralt  22733  mdetralt2  22734  mdetunilem1  22737  mdetunilem2  22738  mdetunilem3  22739  mdetunilem4  22740  mdetunilem9  22745  smadiadetr  22800  pmatcoe1fsupp  22826  mp2pm2mplem4  22934  uniopn  23022  fiinopn  23026  epttop  23134  clsndisj  23200  elcls3  23208  neiptoptop  23256  neiptopnei  23257  cnpval  23361  iscnp  23362  cnpimaex  23381  lmcvg  23387  cnprest  23414  cnprest2  23415  lmss  23423  lmff  23426  t0sep  23449  hausnei  23453  isnrm2  23483  t1sep2  23494  isreg2  23502  iscmp  23513  cmpcov  23514  cmpsublem  23524  cmpsub  23525  tgcmp  23526  uncmp  23528  fiuncmp  23529  hauscmplem  23531  cmpfi  23533  cmpfii  23534  dfconn2  23544  connsuba  23545  connsub  23546  nconnsubb  23548  1stcclb  23569  1stcfb  23570  2ndc1stc  23576  1stcrest  23578  1stcelcls  23586  restnlly  23607  lly1stc  23621  comppfsc  23657  kgenval  23660  kgeni  23662  kgencn2  23682  ptcldmpt  23739  ptclsg  23740  dfac14lem  23742  dfac14  23743  txcnp  23745  ptcnp  23747  hausdiag  23770  txlm  23773  tx1stc  23775  xkococn  23785  cnmpt12  23792  cnmpt22  23799  kqt0lem  23861  isr0  23862  regr1lem2  23865  kqreglem1  23866  r0sep  23873  ptcmpfi  23938  elmptrab  23952  isfil  23972  filss  23978  isufil2  24033  cfinufil  24053  rnelfm  24078  fmfnfmlem2  24080  fmfnfmlem4  24082  flimopn  24100  flimrest  24108  flftg  24121  cnpflf  24126  txflf  24131  fclsopni  24140  fclsrest  24149  fclscf  24150  flimfnfcls  24153  fcfnei  24160  alexsublem  24169  alexsubb  24171  alexsubALTlem3  24174  alexsubALTlem4  24175  alexsubALT  24176  cnextcn  24192  cnextfres1  24193  tgpt0  24244  qustgplem  24246  tsmsi  24259  tsmssubm  24268  tsmsres  24269  tsmsf1o  24270  tsmsxp  24280  ustssel  24331  ust0  24345  ustuqtop4  24369  ucnima  24405  ucncn  24409  iscusp  24423  cuspcvg  24425  imasdsf1olem  24498  blssps  24549  blss  24550  metss  24633  comet  24638  metcnp3  24665  metcnp2  24667  txmetcnp  24672  metuel2  24690  metucn  24696  nrmmetd  24699  nlmvscn  24812  nrginvrcn  24817  nmolb  24842  xrge0tsms  24960  mpomulcn  24994  divcn  24995  fsumcn  24997  elcncf2  25017  cncfi  25021  mulc1cncf  25032  cncfmet  25036  xrhmeo  25073  bndth  25085  nmoleub2lem2  25243  nmoleub3  25246  ipcn  25373  lmmbr  25385  caucfil  25410  pmltpc  25577  ovolfiniun  25628  ovolicc2lem3  25646  ovolicc2  25649  mblsplit  25659  finiunmbl  25671  volfiniun  25674  voliunlem3  25679  ioorinv  25703  ioorcl  25704  dyadmax  25725  dyadmbllem  25726  dyadmbl  25727  opnmbllem  25728  volcn  25733  vitalilem2  25736  vitalilem3  25737  vitali  25740  i1fd  25808  itg2seq  25869  itg2addlem  25885  itgfsum  25954  ellimc3  26006  dvbsss  26029  dvnres  26058  dvmptfsum  26102  dvferm1lem  26111  dvferm2lem  26113  rolle  26117  c1lip1  26124  lhop1lem  26140  lhop1  26141  dvfsumlem2  26154  dvfsumlem4  26156  dvfsumrlim  26158  dvfsum2  26161  ftc1a  26164  ftc1lem6  26168  mdegleb  26189  mdeglt  26190  deg1leb  26220  deg1lt  26222  ply1divex  26262  fta1glem2  26294  fta1g  26295  plyco0  26317  plyeq0lem  26335  coeeq2  26367  dgrle  26368  dgrcolem2  26399  dgrco  26400  plydivlem4  26425  plydivex  26426  fta1lem  26436  fta1  26437  vieta1lem2  26440  vieta1  26441  aalioulem2  26462  aalioulem4  26464  abelth  26569  cxpcn3  26878  rlimcnp  27095  xrlimcnp  27098  cxploglim  27107  scvxcvx  27115  jensen  27118  lgamgulmlem2  27159  wilthlem2  27198  wilthlem3  27199  fta  27209  mpodvdsmulf1o  27323  dvdsmulf1o  27325  perfectlem2  27359  dchrelbas3  27367  dchrelbas4  27372  dchrn0  27379  bcmono  27406  lgsdir2lem4  27457  lgsdchr  27484  gausslemma2dlem0i  27493  lgseisenlem2  27505  lgsquad2lem2  27514  2sqlem6  27552  2sqlem8  27555  2sqlem10  27557  dchrisumlema  27617  dchrisumlem2  27619  dchrisumlem3  27620  nosupprefixmo  27829  noinfprefixmo  27830  nosupcbv  27831  nosupdm  27833  nosupfv  27835  nosupres  27836  nosupbnd1lem1  27837  nosupbnd1lem3  27839  nosupbnd1lem5  27841  nosupbnd2  27845  noinfcbv  27846  noinfdm  27848  noinffv  27850  noinfres  27851  noinfbnd1lem1  27852  noinfbnd1lem3  27854  noinfbnd1lem5  27856  noinfbnd2  27860  nocvxminlem  27912  madebdaylemold  28056  madebdaylemlrcut  28057  madebday  28058  lrrecpo  28099  addsproplem1  28127  addsprop  28134  leadds1  28147  negsproplem1  28186  negsprop  28193  mulsproplemcbv  28273  mulsproplem1  28274  mulsprop  28288  precsexlem8  28372  precsexlem9  28373  precsexlem11  28375  precsex  28376  bdayons  28434  addonbday  28437  onsfi  28514  n0subs  28521  oldfib  28535  eln0zs  28558  bdaypw2n0bndlem  28621  bdaypw2n0bnd  28622  bdayfinbndcbv  28624  bdayfinbndlem1  28625  bdayfinbndlem2  28626  bdayfinbnd  28627  istrkgb  28689  istrkgcb  28690  istrkge  28691  axtgcgrid  28697  axtg5seg  28699  axtgbtwnid  28700  axtgpasch  28701  axtgcont1  28702  axtgeucl  28706  iscgrglt  28748  tgcgr4  28765  axcgrtr  29205  gropd  29321  grstructd  29322  upgredg2vtx  29431  upgredgpr  29432  edglnl  29433  numedglnl  29434  usgredg2vtxeuALT  29512  nbgr2vtx1edg  29640  finsumvtxdg2size  29840  wlkp1lem8  29968  upgrwlkdvdelem  30025  usgr2wlkneq  30045  usgr2pthlem  30052  pthdlem2lem  30056  uspgrn2crct  30097  2pthdlem1  30219  eleclclwwlkn  30367  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  3pthdlem1  30455  eupth2  30530  frgr3vlem1  30564  3vfriswmgrlem  30568  frgrwopreglem4a  30601  frgr2wwlk1  30620  wlkl0  30658  numclwlk2lem2f1o  30670  friendshipgt3  30689  eulplig  30777  nvz  30961  nmobndseqi  31071  nmobndseqiALT  31072  nmlno0  31087  blocnilem  31096  dipdir  31134  dipass  31137  siilem2  31144  ubthlem2  31163  ubth  31165  htth  31210  normpyth  31437  norm3lemt  31444  chlimi  31526  chcompl  31534  omlsii  31695  pjoml  31728  h1de2i  31845  elspansn2  31859  h1datom  31874  pjoml2  31903  pjoml3  31904  lecm  31909  chscllem2  31930  osum  31937  spansncv  31945  pjcjt2  31984  pjopyth  32012  eigre  32127  eigorth  32130  hhcno  32196  hhcnf  32197  cnopc  32205  cnfnc  32222  nmcexi  32318  nmcopexi  32319  nmcfnexi  32343  pjssge0i  32458  hstel2  32511  stj  32527  stri  32549  hstri  32557  stcltr1i  32566  mdbr  32586  mdi  32587  mdbr3  32589  mdbr4  32590  dmdbr  32591  dmdmd  32592  dmdi  32594  dmdbr3  32597  dmdbr4  32598  dmdbr5  32600  mdsl1i  32613  mdslmd1lem3  32619  mdslmd1lem4  32620  mdslmd1i  32621  csmdsymi  32626  cvmd  32628  atss  32638  atom1d  32645  chcv1  32647  hatomic  32652  atord  32680  atcvat2  32681  mddmdin0i  32723  opreu2reuALT  32763  rmoxfrd  32779  ifeqeqx  32828  ssiun2sf  32844  iinabrex  32854  ssrelf  32900  fmptcof2  32942  acunirnmpt  32944  acunirnmpt2  32945  acunirnmpt2f  32946  aciunf1lem  32947  suppovss  32966  fz1nntr  33087  nn0min  33105  fsumiunle  33113  wrdt2ind  33213  ressprs  33226  toslublem  33232  tosglblem  33234  mntoval  33242  ismntd  33244  dfmgc2lem  33255  dfmgc2  33256  xrge0tsmsd  33333  fzto1st  33363  psgnfzto1st  33365  submarchi  33446  archirng  33448  archiexdiv  33450  archiabllem1a  33451  archiabllem2a  33454  archiabl  33458  isarchiofld  33459  gsumvsca1  33486  gsumvsca2  33487  elrgspnlem4  33505  domnpropd  33540  linds2eq  33637  ismxidl  33689  mxidlmax  33692  rprmval  33750  isrprm  33751  rprmdvds  33753  rprmdvdsprod  33768  1arithidomlem1  33769  1arithidom  33771  1arithufdlem3  33780  dfufd2lem  33783  lbsdiflsp0  33960  fedgmullem1  33963  fedgmullem2  33964  fldext2chn  34062  constrmon  34078  submateq  34143  lmatfval  34148  lmatcl  34150  iscref  34178  crefi  34181  pcmplfin  34194  xrge0iifiso  34269  esumcvg  34420  esum2dlem  34426  sigaclcu  34451  sigaclci  34466  unelsiga  34468  unelldsys  34492  sigapildsys  34496  ldgenpisyslem1  34497  fiunelros  34508  measvun  34543  measiun  34552  carsgmon  34648  carsgsigalem  34649  carsgclctunlem2  34653  carsgclctun  34655  pmeasmono  34658  pmeasadd  34659  sibfof  34674  sitgclg  34676  eulerpartlemgvv  34710  signsply0  34882  signstfvneq0  34903  breprexp  34964  hgt749d  34980  istrkg2d  34997  axtgupdim2ALTV  34999  bnj1385  35164  bnj110  35190  bnj222  35215  bnj229  35216  bnj590  35242  bnj865  35255  bnj849  35257  bnj981  35282  bnj1014  35293  bnj1015  35294  bnj1112  35315  bnj1118  35316  bnj1123  35318  bnj1128  35322  bnj1125  35324  bnj1148  35328  bnj1154  35331  bnj1326  35358  bnj1384  35364  bnj1489  35388  bnj1497  35392  funen1cnv  35419  r1filimi  35438  trssfir1om  35446  r1omhfb  35447  setindregs  35465  trssfir1omregs  35471  r1omhfbregs  35472  axpowg  35481  onvf1odlem2  35486  f1resfz0f1d  35503  cplgredgex  35511  acycgrcycl  35537  subfacp1lem6  35575  erdszelem9  35589  kur14lem9  35604  sconnpht  35619  cvmsss2  35664  cvmliftlem7  35681  cvmliftlem10  35684  fmlasuc  35776  gonar  35785  goalr  35787  mclsrcl  35951  mclsssvlem  35952  mclsval  35953  mclsax  35959  mclsind  35960  mclsppslem  35973  iota5f  36114  fununiq  36159  dfon2lem3  36173  dfon2lem4  36174  dfon2lem5  36175  dfon2lem6  36176  dfon2lem7  36177  dfon2lem8  36178  dfon2  36180  btwnconn1lem11  36487  linethru  36543  fwddifnp1  36555  rankelg  36558  rankeq1o  36561  sbequbidv  36614  cbvralvw2  36626  cbvmodavw  36650  cbvsbdavw  36654  cbvsbdavw2  36655  subtr  36713  subtr2  36714  trer  36715  nn0prpwlem  36721  nn0prpw  36722  neibastop2lem  36759  filnetlem4  36780  axtco1from2  36874  axtcond  36877  axuntco  36878  dfttc4lem2  36928  dfttc4  36929  mh-setindnd  36936  regsfromregtco  36937  regsfromsetind  36938  mh-inf3f1  36940  mh-unprimbi  36943  mh-infprim2bi  36946  bj-hbxfrbi  37123  bj-hbyfrbi  37124  bj-ssblem1  37164  bj-ssblem2  37165  bj-ax12  37167  irrdiff  37857  relowlssretop  37896  rdgeqoa  37903  rdgssun  37911  exrecfnlem  37912  finxpreclem6  37929  pibp19  37947  pibt2  37950  wl-ax12v2cl  38039  wl-mo3t  38118  wl-sb8mot  38122  wl-sb8motv  38123  finixpnum  38143  matunitlindflem1  38154  ptrest  38157  poimirlem13  38171  poimirlem14  38172  poimirlem17  38175  poimirlem18  38176  poimirlem20  38178  poimirlem21  38179  poimirlem22  38180  poimirlem24  38182  poimirlem25  38183  poimirlem26  38184  poimirlem28  38186  poimirlem30  38188  poimirlem31  38189  poimirlem32  38190  poimir  38191  heicant  38193  mblfinlem1  38195  mblfinlem2  38196  mblfinlem3  38197  voliunnfl  38202  volsupnfl  38203  mbfresfi  38204  itg2addnclem3  38211  ftc1cnnc  38230  ftc1anclem7  38237  ftc1anc  38239  sdclem2  38280  fdc  38283  fdc1  38284  neificl  38291  mettrifi  38295  sstotbnd2  38312  cntotbnd  38334  heibor1lem  38347  bfp  38362  isass  38384  ismgmOLD  38388  isexid2  38393  iscringd  38536  ispridl  38572  pridl  38575  ismaxidl  38578  maxidlmax  38581  ispridlc  38608  pridlc  38609  dmnnzd  38613  relcnveq2  38867  ecin0  38890  elrelscnveq2  39167  elsymrels3  39176  eltrrels3  39202  eleqvrels3  39215  eqvrelqsel  39238  disjimeceqim2  39343  eldisjim3  39353  eldisjlem19  39451  eldisjsim3  39475  axc11n-16  39601  ax12eq  39604  ax12el  39605  ax12inda  39611  ax12v2-o  39612  fsumshftd  39615  riotasv2d  39620  lshpdisj  39650  lsmsatcv  39673  lsat0cv  39696  lcvexchlem4  39700  lcvexchlem5  39701  l1cvpat  39717  isopos  39843  oposlem  39845  isoml  39901  omllaw  39906  isatl  39962  atlex  39979  iscvlat  39986  cvlexch1  39991  glbconN  40040  hlsuprexch  40044  ps-1  40140  3atlem5  40150  psubspi  40410  llnexchb2  40532  elpcliN  40556  pclfinclN  40613  ldilval  40776  ltrnfset  40780  ltrnset  40781  ltrnu  40784  trlfset  40823  trlset  40824  trlval2  40826  cdleme25cv  41021  cdleme31so  41042  cdleme31fv  41053  cdlemefrs29bpre0  41059  cdleme32fva  41100  cdleme40v  41132  trlord  41232  cdlemkid3N  41596  cdlemkid4  41597  dihffval  41893  dihfval  41894  dihval  41895  lpolconN  42150  mapdordlem2  42300  hdmapfval  42490  hdmapval  42491  hdmapval2  42495  aks4d1p7  42739  isprimroot  42749  primrootlekpowne0  42761  sticksstones1  42802  sticksstones2  42803  sticksstones10  42811  sticksstones12a  42813  aks6d1c6lem3  42828  indstrd  42849  unitscyglem2  42852  unitscyglem3  42853  unitscyglem4  42854  nnn1suc  42922  fsuppind  43213  eu6w  43299  ismrcd1  43320  ismrcd2  43321  ismrc  43323  isnacs3  43332  nacsfix  43334  mzpcompact2  43374  fphpd  43434  fphpdo  43435  monotuz  43559  monotoddzzfi  43560  monotoddzz  43561  oddcomabszz  43562  zindbi  43564  setindtrs  43643  dford3lem2  43645  ttac  43654  dnnumch1  43662  fnwe2lem2  43669  aomclem3  43674  aomclem6  43677  aomclem8  43679  dfac11  43680  dfac21  43684  islssfg2  43689  hbtlem5  43746  hbt  43748  flcidc  43788  mendlmod  43807  unielss  43836  rababg  44191  elmapintrab  44193  iunrelexpuztr  44336  frege92  44572  frege104  44584  ntrkbimka  44655  ntrk0kbimka  44656  neik0pk1imk0  44664  isotone1  44665  isotone2  44666  ntrclsiso  44684  ntrclskb  44686  ntrneiiso  44708  ntrneik3  44713  ntrneix3  44714  gneispacess2  44763  grur1cld  44847  ismnu  44862  mnuop23d  44867  mnuunid  44878  ismnushort  44902  dvgrat  44913  cvgdvgrat  44914  binomcxplemnotnn0  44957  pm14.122b  45024  sbiota1  45035  relprel  45551  relpfrlem  45553  modelaxreplem1  45578  modelaxreplem2  45579  modelaxrep  45581  omssaxinf2  45588  modelac8prim  45592  permaxinf2lem  45612  permac8prim  45614  nregmodel  45617  fnchoice  45640  fiiuncl  45676  iunincfi  45703  disjf1  45792  wessf1ornlem  45794  disjinfi  45801  axccdom  45829  dmrelrnrel  45833  axccd  45835  monoords  45907  fperiodmullem  45913  supxrgere  45940  supxrgelem  45944  supxrge  45945  xrlexaddrp  45959  infxr  45973  infleinf  45978  supxrleubrnmptf  46056  monoordxrv  46086  monoordxr  46087  monoord2xr  46089  fsummulc1f  46178  fsumnncl  46179  fsumf1of  46181  fsumreclf  46183  fsumlessf  46184  fsumsermpt  46186  fmul01  46187  fmulcl  46188  fmuldfeqlem1  46189  fmuldfeq  46190  fmul01lt1lem1  46191  fmul01lt1lem2  46192  fprodexp  46201  fprodabs2  46202  fprodcnlem  46206  climmulf  46211  climexp  46212  climsuse  46215  climrecf  46216  climinff  46218  climaddf  46222  mullimc  46223  mullimcf  46230  limcperiod  46235  sumnnodd  46237  lptre2pt  46245  limsupre  46246  neglimc  46252  addlimc  46253  0ellimcdiv  46254  limclner  46256  climsubmpt  46265  climreclf  46269  climeldmeqmpt  46273  climfveqmpt  46276  fnlimfvre  46279  climfveqf  46285  climfveqmpt3  46287  climeldmeqf  46288  limsupref  46290  limsupbnd1f  46291  climeqf  46293  climeldmeqmpt3  46294  climinf2  46312  limsupubuz  46318  climinf2mpt  46319  climinfmpt  46320  limsupmnf  46326  limsupequz  46328  limsupre2  46330  limsupequzmptf  46336  limsupre3  46338  lmbr3  46352  cnrefiisp  46435  xlimxrre  46436  xlimmnfvlem1  46437  xlimpnfvlem1  46441  climxlim2lem  46450  cncfshift  46479  cncfperiod  46484  icccncfext  46492  fprodcncf  46505  fperdvper  46524  dvmptmulf  46542  dvnmptdivc  46543  dvnmul  46548  dvmptfprod  46550  dvnprodlem1  46551  dvnprodlem2  46552  dvnprodlem3  46553  iblspltprt  46578  itgspltprt  46584  stoweidlem3  46608  stoweidlem4  46609  stoweidlem6  46611  stoweidlem8  46613  stoweidlem15  46620  stoweidlem16  46621  stoweidlem17  46622  stoweidlem19  46624  stoweidlem20  46625  stoweidlem22  46627  stoweidlem23  46628  stoweidlem26  46631  stoweidlem27  46632  stoweidlem30  46635  stoweidlem31  46636  stoweidlem32  46637  stoweidlem34  46639  stoweidlem35  46640  stoweidlem42  46647  stoweidlem43  46648  stoweidlem48  46653  stoweidlem50  46655  stoweidlem51  46656  stoweidlem57  46662  stoweidlem59  46664  stoweidlem62  46667  wallispilem3  46672  dirkercncflem2  46709  fourierdlem11  46723  fourierdlem12  46724  fourierdlem15  46727  fourierdlem16  46728  fourierdlem21  46733  fourierdlem34  46746  fourierdlem41  46753  fourierdlem42  46754  fourierdlem46  46757  fourierdlem48  46759  fourierdlem49  46760  fourierdlem50  46761  fourierdlem51  46762  fourierdlem68  46779  fourierdlem71  46782  fourierdlem72  46783  fourierdlem73  46784  fourierdlem76  46787  fourierdlem79  46790  fourierdlem81  46792  fourierdlem83  46794  fourierdlem86  46797  fourierdlem89  46800  fourierdlem90  46801  fourierdlem91  46802  fourierdlem92  46803  fourierdlem94  46805  fourierdlem97  46808  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  fourierdlem112  46823  fourierdlem113  46824  etransclem2  46841  etransclem46  46885  salunicl  46921  saluncl  46922  intsaluni  46934  dfsalgen2  46946  sge0f1o  46987  sge0lempt  47015  sge0iunmptlemfi  47018  sge0p1  47019  sge0fodjrnlem  47021  sge0iunmpt  47023  sge0ltfirpmpt2  47031  sge0isummpt2  47037  sge0xaddlem2  47039  sge0xadd  47040  nnfoctbdjlem  47060  meadjuni  47062  meadjiun  47071  voliunsge0lem  47077  meaiuninclem  47085  meaiunincf  47088  meaiuninc3v  47089  meaiuninc3  47090  meaiininclem  47091  meaiininc  47092  omeunile  47110  isomenndlem  47135  ovn0lem  47170  ovnsubaddlem1  47175  hoidmvlelem2  47201  hoidmvlelem3  47202  hoidmvlelem4  47203  hoidmvle  47205  hspmbllem2  47232  hoimbl2  47270  vonhoire  47277  vonicclem2  47289  vonn0ioo2  47295  vonn0icc2  47297  salpreimagelt  47312  salpreimalegt  47314  pimdecfgtioc  47320  pimincfltioc  47321  pimincfltioo  47323  salpreimagtge  47330  salpreimaltle  47331  salpreimagtlt  47335  incsmf  47347  decsmf  47372  smflimlem1  47376  smflimlem2  47377  smflimlem3  47378  smflimlem4  47379  smfpimcclem  47412  funressnmo  47671  fcoresf1  47694  aiota0def  47721  euoreqb  47734  2reu8i  47738  2reuimp0  47739  funressndmafv2rn  47848  funressnbrafv2  47869  funbrafv2  47872  smonoord  48002  elsetpreimafvbi  48028  iccpartgt  48064  iccelpart  48070  iccpartiun  48071  icceuelpartlem  48072  icceuelpart  48073  iccpartnel  48075  fargshiftf1  48078  ichexmpl2  48107  ichnreuop  48109  ichreuopeq  48110  sprsymrelfolem2  48130  prproropf1olem4  48143  paireqne  48148  reupr  48159  reuopreuprim  48163  fmtnofac2  48209  fmtnofac1  48210  prmdvdsfmtnof1lem2  48225  perfectALTVlem2  48375  nfermltl8rev  48395  nfermltl2rev  48396  sbgoldbwt  48430  sbgoldbst  48431  sgoldbeven3prm  48436  sbgoldbm  48437  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  evengpop3  48451  evengpoap3  48452  bgoldbnnsum3prm  48457  bgoldbtbndlem4  48461  bgoldbtbnd  48462  tgblthelfgott  48468  tgoldbach  48470  grimuhgr  48540  grimcnv  48541  isuspgrimlem  48548  isubgr3stgrlem4  48622  isubgr3stgrlem6  48624  isubgr3stgrlem7  48625  gpgedg2ov  48719  gpgedg2iv  48720  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  pgnbgreunbgrlem2lem3  48769  pgnbgreunbgrlem5lem1  48773  pgnbgreunbgrlem5lem2  48774  pgnbgreunbgrlem5lem3  48775  pgnbgreunbgr  48778  ply1mulgsumlem2  49051  islininds  49110  linindslinci  49112  lindslinindsimp1  49121  linds0  49129  lindsrng01  49132  snlindsntorlem  49134  snlindsntor  49135  ldepsnlinc  49172  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  nn0sumshdiglem1  49285  nn0sumshdiglem2  49286  nn0sumshdig  49287  itschlc0yqe  49424  f1mo  49515  iscnrm3lem5  49599  iscnrm3r  49610  isprsd  49617  lubeldm2d  49620  glbeldm2d  49621  joindm2  49630  meetdm2  49632  ipolublem  49648  ipolub  49650  ipoglblem  49651  ipoglb  49653  oppcendc  49680  oppcthinendcALT  50103  functhinclem2  50107  fullthinc  50112  fullthinc2  50113  euendfunc  50188  bnd2d  50343  setrec1lem1  50349  setrec1lem4  50352  setrec2fun  50354  alsbid  50464  cbvals  50467