Theorem imbi12d 346

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbi12  348  ifpbi123d  1090  nfbiit  1871  nfbidv  1942  rename-sb  2089  nfbidf  2259  cbvsbvf  2394  drnf1v  2402  drnf1  2474  mo4  2593  cbvmovw  2629  cbvmow  2630  axextg  2736  rspw  3239  cbvralvw  3240  cbvralfw  3302  raleqbidv  3336  cbvraldva2  3338  sbralie  3340  sbralieOLD  3342  cbvralf  3347  ralcom2  3364  vtoclgaf  3540  vtoclga  3541  rspct  3567  rspc  3569  rspc2gv  3591  rexraleqim  3606  ralab2  3660  nelrdva  3668  mob2  3678  mob  3680  morex  3682  reu7  3695  reu8  3696  reu2eqd  3699  cdeqim  3736  sbcimg  3792  sbcim1  3797  sbceqal  3805  csbhypf  3880  cbvralcsf  3894  dfssf  3927  reldisj  4407  ralidmw  4470  reusngf  4633  rexreusng  4638  reuprg0  4661  elpreqpr  4825  unissb  4899  intss1  4921  intmin  4926  dftr2c  5210  trel  5215  zfpow  5323  reusv2lem4  5358  reusv3i  5361  rext  5415  opth  5444  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  poeq1  5558  pocl  5563  swopolem  5565  swopo  5566  isso2i  5592  vtoclr  5710  poinxp  5728  posn  5733  ssrel  5755  ssrel2  5757  ssrelrel  5768  relop  5822  cotrg  6098  cnvsym  6101  reu3op  6279  reuop  6280  dfpo2  6283  preddowncl  6319  frpoinsg  6330  ordelord  6368  iota5  6504  dffun2  6531  sbcfung  6545  funopg  6555  brprcneu  6857  brprcneuALT  6858  tz6.12f  6892  funbrfv  6915  ssimaexg  6953  fvmptf  6997  fvelrn  7057  fprg  7138  dff13f  7239  f1veqaeq  7240  fpropnf1  7251  f1ounsn  7256  nf1const  7288  soisores  7311  soisoi  7312  isofrlem  7324  isopolem  7329  weniso  7338  riota5f  7381  imbrov2fvoveq  7421  oprabidw  7427  oprabid  7428  f1opr  7452  ovmpos  7544  ov2gf  7545  ov3  7559  caovcan  7600  caovordig  7601  caofrss  7699  caoftrn  7701  tfisg  7834  tfis  7835  tfisi  7839  tfindsg  7841  tfindsg2  7842  tfindes  7843  dfom2  7848  limomss  7851  nnlim  7860  peano5  7874  findsg  7878  findes  7881  resf1extb  7915  f1oweALT  7953  dfoprab4f  8037  offval22  8067  f1o2ndf1  8101  frxp  8106  poxp  8108  frpoins3xpg  8120  frpoins3xp3g  8121  poxp2  8123  frxp2  8124  xpord2indlem  8127  poxp3  8130  frxp3  8131  xpord3inddlem  8134  suppfnss  8169  onfununi  8312  smoel  8331  smogt  8338  tfrlem1  8346  tz7.48lem  8412  tz7.49  8416  oawordeu  8524  omordi  8535  oeordi  8557  nnmordi  8601  omabs  8621  nneob  8626  omsmolem  8627  qsel  8778  eroveu  8794  ecopovtrn  8802  ixpsnf1o  8920  fundmeng  9013  sbth  9069  limensuc  9126  findcard  9132  findcard2  9133  findcard2d  9135  pssnn  9137  ssfi  9141  sbthfi  9167  nneneq  9174  php  9175  unxpdom  9203  findcard3  9227  ac6sfi  9228  frfi  9229  domunfican  9266  fiint  9271  iunfi  9286  finsschain  9302  dffi3  9377  marypha1lem  9379  marypha1  9380  supeq3  9395  supeq123d  9396  supmo  9398  suplub  9406  supisolem  9420  eqinf  9431  infval  9433  infmo  9443  ordiso2  9463  ordtypelem7  9472  wemaplem1  9494  wemaplem2  9495  zfregcl  9542  zfregclOLD  9543  elirrv  9545  elirrvOLD  9546  inf0  9576  inf3lem1  9583  zfinf  9594  axinf2  9595  dfom3  9602  elom3  9603  cantnfval2  9624  cantnfle  9626  cantnflt  9627  cantnfp1lem3  9635  oemapvali  9639  cantnflem1c  9642  cantnflem1  9644  cantnf  9648  wemapwe  9652  cnfcom  9655  ttrclss  9675  ttrclselem2  9681  setind  9702  setinds  9704  frmin  9707  frinsg  9709  r1sdom  9732  r1ordg  9736  rankonidlem  9786  rankunb  9808  bnd2  9851  infxpenlem  9969  infxpenc2  9978  dfac8alem  9985  dfac8clem  9988  indcardi  9997  alephordi  10030  alephinit  10051  alephfp  10064  aceq3lem  10076  dfac5lem4  10082  dfac5lem4OLD  10084  dfac5  10085  dfac2b  10087  dfac9  10093  dfac12lem2  10101  dfac12lem3  10102  kmlem1  10107  kmlem4  10110  kmlem10  10116  kmlem12  10118  kmlem13  10119  pwsdompw  10159  ackbij1lem16  10190  cfslb2n  10225  cfsmolem  10227  sornom  10234  fin2i  10252  infpssrlem4  10263  isfin2-2  10276  isfin3ds  10286  fin23lem17  10295  fin23lem32  10301  fin23lem34  10303  fin23lem35  10304  fin23lem39  10307  fin23lem41  10309  isf32lem2  10311  isf33lem  10323  isf34lem4  10334  isf34lem6  10337  fin1a2lem10  10366  axcc2lem  10393  axcc3  10395  axcc4dom  10398  dominf  10402  axdc2lem  10405  axdc3lem2  10408  ac6sg  10445  zorn2lem7  10459  zornn0g  10462  ttukeylem5  10470  ttukeylem6  10471  axdclem  10476  dominfac  10531  axrepndlem1  10550  axrepndlem2  10551  axunndlem1  10553  axunnd  10554  axpowndlem2  10556  axpowndlem3  10557  axpowndlem4  10558  axregndlem2  10561  axregnd  10562  axinfndlem1  10563  axinfnd  10564  axacndlem4  10568  axacndlem5  10569  axacnd  10570  zfcndpow  10574  zfcndinf  10576  fpwwe2lem4  10592  fpwwe2lem7  10595  fpwwe2lem11  10599  pwfseqlem4a  10619  pwfseqlem4  10620  pwfseqlem5  10621  pwfseq  10622  wunfi  10679  wunex2  10696  inar1  10733  rankcf  10735  tskord  10738  grudomon  10775  grur1a  10777  axgroth6  10786  axgroth3  10789  axgroth4  10790  eltskm  10801  indpi  10865  pinq  10885  nqereu  10887  prcdnq  10951  prnmax  10953  ltsopr  10990  prlem936  11005  ltsosr  11052  recexsrlem  11061  mulgt0sr  11063  map2psrpr  11068  supsrlem  11069  axrrecex  11121  axpre-lttrn  11124  axpre-mulgt0  11126  axpre-sup  11127  axsup  11258  dedekind  11346  ltordlem  11712  ltord1  11713  wloglei  11719  squeeze0  12095  infm3  12151  nnsub  12257  nnunb  12477  peano5uzti  12663  fzind  12671  uzind4s  12909  uzind4s2  12910  zmax  12946  zbtwnre  12947  xmulasslem  13288  xrsupsslem  13310  xrinfmsslem  13311  xrub  13315  infmremnf  13347  injresinj  13797  om2uzlti  13963  uzindi  13995  axdc4uz  13997  ssnn0fi  13998  rabssnn0fi  13999  suppssfz  14007  seqp1  14029  seqcl2  14033  seqfveq2  14037  seqshft2  14041  monoord  14045  seqsplit  14048  seqf1olem2  14055  seqf1o  14056  seqid2  14061  seqhomo  14062  seqof2  14073  expcl2lem  14086  facdiv  14300  facwordi  14302  faclbnd4lem2  14307  hashnn0n0nn  14404  hashf1lem2  14469  seqcoll  14477  fi1uzind  14520  brfi1indALT  14523  wrdind  14735  wrd2ind  14736  swrdccatin1  14738  swrdccat3blem  14752  reuccatpfxs1lem  14759  repswccat  14799  cshf1  14823  trclfvcotr  15022  relexprelg  15051  rtrclreclem4  15074  relexpindlem  15076  ello1mpt  15548  o1co  15613  o1compt  15614  rlimcn3  15617  climcn2  15620  subcn2  15622  o1of2  15640  fsumclf  15765  fsumsplitf  15769  fsumsplit1  15772  fsum2d  15798  modfsummod  15822  fsumabs  15829  telfsumo  15830  fsumrlim  15839  fsumo1  15840  o1fsum  15841  fsumiun  15849  prodfdiv  15926  fprod2d  16011  fproddivf  16017  fprodsplitf  16018  fprodsplit1f  16020  rpnnen2lem10  16255  sqrt2irr  16281  dvdsle  16344  divalglem7  16433  divalglem8  16434  ndvdssub  16443  gcdcllem1  16533  dfgcd2  16580  algcvg  16610  algcvga  16613  algfx  16614  lcmgcdlem  16640  lcmdvds  16642  lcmf  16667  lcmfunsnlem1  16671  lcmfunsnlem2lem1  16672  lcmfunsnlem  16675  lcmfdvds  16676  lcmfun  16679  coprmgcdb  16683  coprmdvds1  16686  coprmdvds2  16688  coprmprod  16695  coprmproddvds  16697  prmind2  16719  dvdsprime  16721  nprm  16722  dvdsprm  16738  exprmfct  16739  coprm  16746  isprm6  16749  prmfac1  16755  eulerthlem2  16817  pcqmul  16889  pcqcl  16892  pc2dvds  16915  pcz  16917  prmpwdvds  16940  infpn2  16949  vdwlem12  17028  ramub2  17050  rami  17051  ramcl  17065  prmdvdsprmop  17079  prmlem0  17141  mreintcl  17623  ismred2  17631  mrissmrcd  17672  mreexexlemd  17676  iscatd2  17713  moni  17769  yoniso  18317  isprs  18328  prslem  18329  drsdirfi  18337  ispos  18346  posi  18349  isposd  18354  pospropd  18357  lubfval  18380  lublecllem  18390  glbfval  18393  joinle  18416  meetle  18430  poslubmo  18441  posglbmo  18442  resspos  18461  lubl  18544  lubun  18547  clatleglb  18550  ipodrsima  18573  acsdrsel  18575  isacs4lem  18576  isacs5lem  18577  acsdrscl  18578  mreclatBAD  18595  pslem  18604  dirtr  18634  chnind  18653  mndind  18862  mhmlem  19104  isnsg2  19197  ghmf1  19286  orbsta  19353  symgextf1  19461  gsmsymgrfix  19468  gsmsymgreq  19472  symggen  19510  psgnunilem4  19537  sylow1lem1  19638  sylow2alem2  19658  sylow2a  19659  lsmmod  19715  lsmdisj2  19722  efgsrel  19774  efgredlemd  19784  efgredlem  19787  efgred  19788  gsumzaddlem  19961  gsummptnn0fz  20026  gsummptnn0fzfv  20027  telgsumfzs  20029  telgsums  20033  dprdval  20045  dprddisj2  20081  ablfac1eulem  20114  pgpfac1lem1  20116  pgpfac1lem5  20121  pgpfac1  20122  pgpfaclem2  20124  pgpfac  20126  isomnd  20163  omndadd  20168  gsumle  20185  irredmul  20478  islring  20590  lringuplu  20594  rrgval  20747  rrgeq0i  20749  isdomn  20755  domneq0  20758  isdomn4  20766  domnlcanb  20770  domnrcanb  20772  isdrngrd  20816  isdrngrdOLD  20818  sdrgacs  20850  isorng  20910  orngmul  20914  islbs3  21225  rngqiprngimf1lem  21364  cnsubrglem  21469  prmirredlem  21524  znfld  21612  znrrg  21617  cygznlem3  21621  isphl  21680  ipeq0  21690  isphld  21706  phlpropd  21707  lsmcss  21744  frlmphl  21833  frlmup1  21850  lindfrn  21873  islindf4  21890  islindf5  21891  mplsubglem  22050  mpllsslem  22051  mplcoe1  22090  mplcoe5  22093  mpfind  22168  ismhp3  22207  coe1fzgsumd  22367  gsummoncoe1  22371  pf1ind  22418  evl1gsumd  22420  dmatelnd  22556  mat1scmat  22599  mdetdiaglem  22658  mdetralt  22668  mdetralt2  22669  mdetunilem1  22672  mdetunilem2  22673  mdetunilem3  22674  mdetunilem4  22675  mdetunilem9  22680  smadiadetr  22735  pmatcoe1fsupp  22761  mp2pm2mplem4  22869  uniopn  22957  fiinopn  22961  epttop  23069  clsndisj  23135  elcls3  23143  neiptoptop  23191  neiptopnei  23192  cnpval  23296  iscnp  23297  cnpimaex  23316  lmcvg  23322  cnprest  23349  cnprest2  23350  lmss  23358  lmff  23361  t0sep  23384  hausnei  23388  isnrm2  23418  t1sep2  23429  isreg2  23437  iscmp  23448  cmpcov  23449  cmpsublem  23459  cmpsub  23460  tgcmp  23461  uncmp  23463  fiuncmp  23464  hauscmplem  23466  cmpfi  23468  cmpfii  23469  dfconn2  23479  connsuba  23480  connsub  23481  nconnsubb  23483  1stcclb  23504  1stcfb  23505  2ndc1stc  23511  1stcrest  23513  1stcelcls  23521  restnlly  23542  lly1stc  23556  comppfsc  23592  kgenval  23595  kgeni  23597  kgencn2  23617  ptcldmpt  23674  ptclsg  23675  dfac14lem  23677  dfac14  23678  txcnp  23680  ptcnp  23682  hausdiag  23705  txlm  23708  tx1stc  23710  xkococn  23720  cnmpt12  23727  cnmpt22  23734  kqt0lem  23796  isr0  23797  regr1lem2  23800  kqreglem1  23801  r0sep  23808  ptcmpfi  23873  elmptrab  23887  isfil  23907  filss  23913  isufil2  23968  cfinufil  23988  rnelfm  24013  fmfnfmlem2  24015  fmfnfmlem4  24017  flimopn  24035  flimrest  24043  flftg  24056  cnpflf  24061  txflf  24066  fclsopni  24075  fclsrest  24084  fclscf  24085  flimfnfcls  24088  fcfnei  24095  alexsublem  24104  alexsubb  24106  alexsubALTlem3  24109  alexsubALTlem4  24110  alexsubALT  24111  cnextcn  24127  cnextfres1  24128  tgpt0  24179  qustgplem  24181  tsmsi  24194  tsmssubm  24203  tsmsres  24204  tsmsf1o  24205  tsmsxp  24215  ustssel  24266  ust0  24280  ustuqtop4  24304  ucnima  24340  ucncn  24344  iscusp  24358  cuspcvg  24360  imasdsf1olem  24433  blssps  24484  blss  24485  metss  24568  comet  24573  metcnp3  24600  metcnp2  24602  txmetcnp  24607  metuel2  24625  metucn  24631  nrmmetd  24634  nlmvscn  24747  nrginvrcn  24752  nmolb  24777  xrge0tsms  24895  mpomulcn  24929  divcn  24930  fsumcn  24932  elcncf2  24952  cncfi  24956  mulc1cncf  24967  cncfmet  24971  xrhmeo  25008  bndth  25020  nmoleub2lem2  25178  nmoleub3  25181  ipcn  25308  lmmbr  25320  caucfil  25345  pmltpc  25512  ovolfiniun  25563  ovolicc2lem3  25581  ovolicc2  25584  mblsplit  25594  finiunmbl  25606  volfiniun  25609  voliunlem3  25614  ioorinv  25638  ioorcl  25639  dyadmax  25660  dyadmbllem  25661  dyadmbl  25662  opnmbllem  25663  volcn  25668  vitalilem2  25671  vitalilem3  25672  vitali  25675  i1fd  25743  itg2seq  25804  itg2addlem  25820  itgfsum  25889  ellimc3  25941  dvbsss  25964  dvnres  25993  dvmptfsum  26037  dvferm1lem  26046  dvferm2lem  26048  rolle  26052  c1lip1  26059  lhop1lem  26075  lhop1  26076  dvfsumlem2  26089  dvfsumlem4  26091  dvfsumrlim  26093  dvfsum2  26096  ftc1a  26099  ftc1lem6  26103  mdegleb  26124  mdeglt  26125  deg1leb  26155  deg1lt  26157  ply1divex  26197  fta1glem2  26229  fta1g  26230  plyco0  26252  plyeq0lem  26270  coeeq2  26302  dgrle  26303  dgrcolem2  26334  dgrco  26335  plydivlem4  26360  plydivex  26361  fta1lem  26371  fta1  26372  vieta1lem2  26375  vieta1  26376  aalioulem2  26397  aalioulem4  26399  abelth  26504  cxpcn3  26813  rlimcnp  27030  xrlimcnp  27033  cxploglim  27042  scvxcvx  27050  jensen  27053  lgamgulmlem2  27094  wilthlem2  27133  wilthlem3  27134  fta  27144  mpodvdsmulf1o  27258  dvdsmulf1o  27260  perfectlem2  27294  dchrelbas3  27302  dchrelbas4  27307  dchrn0  27314  bcmono  27341  lgsdir2lem4  27392  lgsdchr  27419  gausslemma2dlem0i  27428  lgseisenlem2  27440  lgsquad2lem2  27449  2sqlem6  27487  2sqlem8  27490  2sqlem10  27492  dchrisumlema  27552  dchrisumlem2  27554  dchrisumlem3  27555  nosupprefixmo  27764  noinfprefixmo  27765  nosupcbv  27766  nosupdm  27768  nosupfv  27770  nosupres  27771  nosupbnd1lem1  27772  nosupbnd1lem3  27774  nosupbnd1lem5  27776  nosupbnd2  27780  noinfcbv  27781  noinfdm  27783  noinffv  27785  noinfres  27786  noinfbnd1lem1  27787  noinfbnd1lem3  27789  noinfbnd1lem5  27791  noinfbnd2  27795  nocvxminlem  27847  madebdaylemold  27991  madebdaylemlrcut  27992  madebday  27993  lrrecpo  28034  addsproplem1  28062  addsprop  28069  leadds1  28082  negsproplem1  28121  negsprop  28128  mulsproplemcbv  28208  mulsproplem1  28209  mulsprop  28223  precsexlem8  28307  precsexlem9  28308  precsexlem11  28310  precsex  28311  bdayons  28369  addonbday  28372  onsfi  28449  n0subs  28456  oldfib  28470  eln0zs  28493  bdaypw2n0bndlem  28556  bdaypw2n0bnd  28557  bdayfinbndcbv  28559  bdayfinbndlem1  28560  bdayfinbndlem2  28561  bdayfinbnd  28562  istrkgb  28624  istrkgcb  28625  istrkge  28626  axtgcgrid  28632  axtg5seg  28634  axtgbtwnid  28635  axtgpasch  28636  axtgcont1  28637  axtgeucl  28641  iscgrglt  28683  tgcgr4  28700  axcgrtr  29116  gropd  29232  grstructd  29233  upgredg2vtx  29342  upgredgpr  29343  edglnl  29344  numedglnl  29345  usgredg2vtxeuALT  29423  nbgr2vtx1edg  29551  finsumvtxdg2size  29751  wlkp1lem8  29879  upgrwlkdvdelem  29936  usgr2wlkneq  29956  usgr2pthlem  29963  pthdlem2lem  29967  uspgrn2crct  30008  2pthdlem1  30130  eleclclwwlkn  30278  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  3pthdlem1  30366  eupth2  30441  frgr3vlem1  30475  3vfriswmgrlem  30479  frgrwopreglem4a  30512  frgr2wwlk1  30531  wlkl0  30569  numclwlk2lem2f1o  30581  friendshipgt3  30600  eulplig  30688  nvz  30872  nmobndseqi  30982  nmobndseqiALT  30983  nmlno0  30998  blocnilem  31007  dipdir  31045  dipass  31048  siilem2  31055  ubthlem2  31074  ubth  31076  htth  31121  normpyth  31348  norm3lemt  31355  chlimi  31437  chcompl  31445  omlsii  31606  pjoml  31639  h1de2i  31756  elspansn2  31770  h1datom  31785  pjoml2  31814  pjoml3  31815  lecm  31820  chscllem2  31841  osum  31848  spansncv  31856  pjcjt2  31895  pjopyth  31923  eigre  32038  eigorth  32041  hhcno  32107  hhcnf  32108  cnopc  32116  cnfnc  32133  nmcexi  32229  nmcopexi  32230  nmcfnexi  32254  pjssge0i  32369  hstel2  32422  stj  32438  stri  32460  hstri  32468  stcltr1i  32477  mdbr  32497  mdi  32498  mdbr3  32500  mdbr4  32501  dmdbr  32502  dmdmd  32503  dmdi  32505  dmdbr3  32508  dmdbr4  32509  dmdbr5  32511  mdsl1i  32524  mdslmd1lem3  32530  mdslmd1lem4  32531  mdslmd1i  32532  csmdsymi  32537  cvmd  32539  atss  32549  atom1d  32556  chcv1  32558  hatomic  32563  atord  32591  atcvat2  32592  mddmdin0i  32634  opreu2reuALT  32676  rmoxfrd  32692  ifeqeqx  32741  ssiun2sf  32759  iinabrex  32769  ssrelf  32817  fmptcof2  32859  acunirnmpt  32861  acunirnmpt2  32862  acunirnmpt2f  32863  aciunf1lem  32864  suppovss  32883  fz1nntr  33004  nn0min  33023  fsumiunle  33031  wrdt2ind  33131  ressprs  33144  toslublem  33150  tosglblem  33152  mntoval  33160  ismntd  33162  dfmgc2lem  33173  dfmgc2  33174  xrge0tsmsd  33253  fzto1st  33283  psgnfzto1st  33285  submarchi  33366  archirng  33368  archiexdiv  33370  archiabllem1a  33371  archiabllem2a  33374  archiabl  33378  isarchiofld  33379  gsumvsca1  33406  gsumvsca2  33407  elrgspnlem4  33426  domnpropd  33461  domnlcanOLD  33464  linds2eq  33567  isprmidl  33624  prmidl  33626  prmidlc  33634  prmidlprop  33635  ssdifidlprm  33645  ismxidl  33650  mxidlmax  33653  rprmval  33712  isrprm  33713  rprmdvds  33715  rprmdvdsprod  33730  1arithidomlem1  33731  1arithidom  33733  1arithufdlem3  33742  dfufd2lem  33745  lbsdiflsp0  33923  fedgmullem1  33926  fedgmullem2  33927  fldext2chn  34025  constrmon  34041  submateq  34106  lmatfval  34111  lmatcl  34113  iscref  34141  crefi  34144  pcmplfin  34157  xrge0iifiso  34232  esumcvg  34383  esum2dlem  34389  sigaclcu  34414  sigaclci  34429  unelsiga  34431  unelldsys  34455  sigapildsys  34459  ldgenpisyslem1  34460  fiunelros  34471  measvun  34506  measiun  34515  carsgmon  34611  carsgsigalem  34612  carsgclctunlem2  34616  carsgclctun  34618  pmeasmono  34621  pmeasadd  34622  sibfof  34637  sitgclg  34639  eulerpartlemgvv  34673  signsply0  34845  signstfvneq0  34866  breprexp  34927  hgt749d  34943  istrkg2d  34960  axtgupdim2ALTV  34962  bnj1385  35127  bnj110  35153  bnj222  35178  bnj229  35179  bnj590  35205  bnj865  35218  bnj849  35220  bnj981  35245  bnj1014  35256  bnj1015  35257  bnj1112  35278  bnj1118  35279  bnj1123  35281  bnj1128  35285  bnj1125  35287  bnj1148  35291  bnj1154  35294  bnj1326  35321  bnj1384  35327  bnj1489  35351  bnj1497  35355  funen1cnv  35382  r1filimi  35399  trssfir1om  35407  r1omhfb  35408  setindregs  35426  trssfir1omregs  35432  r1omhfbregs  35433  axpowg  35442  onvf1odlem2  35447  f1resfz0f1d  35464  cplgredgex  35471  acycgrcycl  35497  subfacp1lem6  35535  erdszelem9  35549  kur14lem9  35564  sconnpht  35579  cvmsss2  35624  cvmliftlem7  35641  cvmliftlem10  35644  fmlasuc  35736  gonar  35745  goalr  35747  mclsrcl  35911  mclsssvlem  35912  mclsval  35913  mclsax  35919  mclsind  35920  mclsppslem  35933  iota5f  36074  fununiq  36119  dfon2lem3  36133  dfon2lem4  36134  dfon2lem5  36135  dfon2lem6  36136  dfon2lem7  36137  dfon2lem8  36138  dfon2  36140  btwnconn1lem11  36447  linethru  36503  fwddifnp1  36515  rankelg  36518  rankeq1o  36521  sbequbidv  36574  cbvralvw2  36586  cbvmodavw  36610  cbvsbdavw  36614  cbvsbdavw2  36615  subtr  36674  subtr2  36675  trer  36676  nn0prpwlem  36682  nn0prpw  36683  neibastop2lem  36720  filnetlem4  36741  axtco1from2  36835  axtcond  36838  axuntco  36839  dfttc4lem2  36889  dfttc4  36890  mh-setindnd  36897  regsfromregtco  36898  regsfromsetind  36899  mh-inf3f1  36901  mh-unprimbi  36904  mh-infprim2bi  36907  bj-hbxfrbi  37085  bj-hbyfrbi  37086  bj-ssblem1  37126  bj-ssblem2  37127  bj-ax12  37129  irrdiff  37818  relowlssretop  37857  rdgeqoa  37864  rdgssun  37872  exrecfnlem  37873  finxpreclem6  37890  pibp19  37908  pibt2  37911  wl-ax12v2cl  38000  wl-mo3t  38079  wl-sb8mot  38083  wl-sb8motv  38084  finixpnum  38104  matunitlindflem1  38115  ptrest  38118  poimirlem13  38132  poimirlem14  38133  poimirlem17  38136  poimirlem18  38137  poimirlem20  38139  poimirlem21  38140  poimirlem22  38141  poimirlem24  38143  poimirlem25  38144  poimirlem26  38145  poimirlem28  38147  poimirlem30  38149  poimirlem31  38150  poimirlem32  38151  poimir  38152  heicant  38154  mblfinlem1  38156  mblfinlem2  38157  mblfinlem3  38158  voliunnfl  38163  volsupnfl  38164  mbfresfi  38165  itg2addnclem3  38172  ftc1cnnc  38191  ftc1anclem7  38198  ftc1anc  38200  sdclem2  38241  fdc  38244  fdc1  38245  neificl  38252  mettrifi  38256  sstotbnd2  38273  cntotbnd  38295  heibor1lem  38308  bfp  38323  isass  38345  ismgmOLD  38349  isexid2  38354  iscringd  38497  ispridl  38533  pridl  38536  ismaxidl  38539  maxidlmax  38542  ispridlc  38569  pridlc  38570  dmnnzd  38574  relcnveq2  38828  ecin0  38851  elrelscnveq2  39128  elsymrels3  39137  eltrrels3  39163  eleqvrels3  39176  eqvrelqsel  39199  disjimeceqim2  39304  eldisjim3  39314  eldisjlem19  39412  eldisjsim3  39436  axc11n-16  39562  ax12eq  39565  ax12el  39566  ax12inda  39572  ax12v2-o  39573  fsumshftd  39576  riotasv2d  39581  lshpdisj  39611  lsmsatcv  39634  lsat0cv  39657  lcvexchlem4  39661  lcvexchlem5  39662  l1cvpat  39678  isopos  39804  oposlem  39806  isoml  39862  omllaw  39867  isatl  39923  atlex  39940  iscvlat  39947  cvlexch1  39952  glbconN  40001  hlsuprexch  40005  ps-1  40101  3atlem5  40111  psubspi  40371  llnexchb2  40493  elpcliN  40517  pclfinclN  40574  ldilval  40737  ltrnfset  40741  ltrnset  40742  ltrnu  40745  trlfset  40784  trlset  40785  trlval2  40787  cdleme25cv  40982  cdleme31so  41003  cdleme31fv  41014  cdlemefrs29bpre0  41020  cdleme32fva  41061  cdleme40v  41093  trlord  41193  cdlemkid3N  41557  cdlemkid4  41558  dihffval  41854  dihfval  41855  dihval  41856  lpolconN  42111  mapdordlem2  42261  hdmapfval  42451  hdmapval  42452  hdmapval2  42456  aks4d1p7  42700  isprimroot  42710  primrootlekpowne0  42722  sticksstones1  42763  sticksstones2  42764  sticksstones10  42772  sticksstones12a  42774  aks6d1c6lem3  42789  indstrd  42810  unitscyglem2  42813  unitscyglem3  42814  unitscyglem4  42815  nnn1suc  42881  fsuppind  43172  eu6w  43258  ismrcd1  43279  ismrcd2  43280  ismrc  43282  isnacs3  43291  nacsfix  43293  mzpcompact2  43333  fphpd  43393  fphpdo  43394  monotuz  43518  monotoddzzfi  43519  monotoddzz  43520  oddcomabszz  43521  zindbi  43523  setindtrs  43602  dford3lem2  43604  ttac  43613  dnnumch1  43621  fnwe2lem2  43628  aomclem3  43633  aomclem6  43636  aomclem8  43638  dfac11  43639  dfac21  43643  islssfg2  43648  hbtlem5  43705  hbt  43707  flcidc  43747  mendlmod  43766  unielss  43795  rababg  44150  elmapintrab  44152  iunrelexpuztr  44295  frege92  44531  frege104  44543  ntrkbimka  44614  ntrk0kbimka  44615  neik0pk1imk0  44623  isotone1  44624  isotone2  44625  ntrclsiso  44643  ntrclskb  44645  ntrneiiso  44667  ntrneik3  44672  ntrneix3  44673  gneispacess2  44722  grur1cld  44808  scottabf  44816  ismnu  44837  mnuop23d  44842  mnuunid  44853  ismnushort  44877  dvgrat  44888  cvgdvgrat  44889  binomcxplemnotnn0  44932  pm14.122b  44999  sbiota1  45010  relprel  45527  relpfrlem  45529  modelaxreplem1  45554  modelaxreplem2  45555  modelaxrep  45557  omssaxinf2  45564  modelac8prim  45568  permaxinf2lem  45588  permac8prim  45590  nregmodel  45593  fnchoice  45609  fiiuncl  45645  iunincfi  45672  disjf1  45761  wessf1ornlem  45763  disjinfi  45770  axccdom  45798  dmrelrnrel  45802  axccd  45804  monoords  45876  fperiodmullem  45882  supxrgere  45909  supxrgelem  45913  supxrge  45914  xrlexaddrp  45928  infxr  45942  infleinf  45947  supxrleubrnmptf  46025  monoordxrv  46055  monoordxr  46056  monoord2xr  46058  fsummulc1f  46147  fsumnncl  46148  fsumf1of  46150  fsumreclf  46152  fsumlessf  46153  fsumsermpt  46155  fmul01  46156  fmulcl  46157  fmuldfeqlem1  46158  fmuldfeq  46159  fmul01lt1lem1  46160  fmul01lt1lem2  46161  fprodexp  46170  fprodabs2  46171  fprodcnlem  46175  climmulf  46180  climexp  46181  climsuse  46184  climrecf  46185  climinff  46187  climaddf  46191  mullimc  46192  mullimcf  46199  limcperiod  46204  sumnnodd  46206  lptre2pt  46214  limsupre  46215  neglimc  46221  addlimc  46222  0ellimcdiv  46223  limclner  46225  climsubmpt  46234  climreclf  46238  climeldmeqmpt  46242  climfveqmpt  46245  fnlimfvre  46248  climfveqf  46254  climfveqmpt3  46256  climeldmeqf  46257  limsupref  46259  limsupbnd1f  46260  climeqf  46262  climeldmeqmpt3  46263  climinf2  46281  limsupubuz  46287  climinf2mpt  46288  climinfmpt  46289  limsupmnf  46295  limsupequz  46297  limsupre2  46299  limsupequzmptf  46305  limsupre3  46307  lmbr3  46321  cnrefiisp  46404  xlimxrre  46405  xlimmnfvlem1  46406  xlimpnfvlem1  46410  climxlim2lem  46419  cncfshift  46448  cncfperiod  46453  icccncfext  46461  fprodcncf  46474  fperdvper  46493  dvmptmulf  46511  dvnmptdivc  46512  dvnmul  46517  dvmptfprod  46519  dvnprodlem1  46520  dvnprodlem2  46521  dvnprodlem3  46522  iblspltprt  46547  itgspltprt  46553  stoweidlem3  46577  stoweidlem4  46578  stoweidlem6  46580  stoweidlem8  46582  stoweidlem15  46589  stoweidlem16  46590  stoweidlem17  46591  stoweidlem19  46593  stoweidlem20  46594  stoweidlem22  46596  stoweidlem23  46597  stoweidlem26  46600  stoweidlem27  46601  stoweidlem30  46604  stoweidlem31  46605  stoweidlem32  46606  stoweidlem34  46608  stoweidlem35  46609  stoweidlem42  46616  stoweidlem43  46617  stoweidlem48  46622  stoweidlem50  46624  stoweidlem51  46625  stoweidlem57  46631  stoweidlem59  46633  stoweidlem62  46636  wallispilem3  46641  dirkercncflem2  46678  fourierdlem11  46692  fourierdlem12  46693  fourierdlem15  46696  fourierdlem16  46697  fourierdlem21  46702  fourierdlem34  46715  fourierdlem41  46722  fourierdlem42  46723  fourierdlem46  46726  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem51  46731  fourierdlem68  46748  fourierdlem71  46751  fourierdlem72  46752  fourierdlem73  46753  fourierdlem76  46756  fourierdlem79  46759  fourierdlem81  46761  fourierdlem83  46763  fourierdlem86  46766  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  fourierdlem92  46772  fourierdlem94  46774  fourierdlem97  46777  fourierdlem103  46783  fourierdlem104  46784  fourierdlem111  46791  fourierdlem112  46792  fourierdlem113  46793  etransclem2  46810  etransclem46  46854  salunicl  46890  saluncl  46891  intsaluni  46903  dfsalgen2  46915  sge0f1o  46956  sge0lempt  46984  sge0iunmptlemfi  46987  sge0p1  46988  sge0fodjrnlem  46990  sge0iunmpt  46992  sge0ltfirpmpt2  47000  sge0isummpt2  47006  sge0xaddlem2  47008  sge0xadd  47009  nnfoctbdjlem  47029  meadjuni  47031  meadjiun  47040  voliunsge0lem  47046  meaiuninclem  47054  meaiunincf  47057  meaiuninc3v  47058  meaiuninc3  47059  meaiininclem  47060  meaiininc  47061  omeunile  47079  isomenndlem  47104  ovn0lem  47139  ovnsubaddlem1  47144  hoidmvlelem2  47170  hoidmvlelem3  47171  hoidmvlelem4  47172  hoidmvle  47174  hspmbllem2  47201  hoimbl2  47239  vonhoire  47246  vonicclem2  47258  vonn0ioo2  47264  vonn0icc2  47266  salpreimagelt  47281  salpreimalegt  47283  pimdecfgtioc  47289  pimincfltioc  47290  pimincfltioo  47292  salpreimagtge  47299  salpreimaltle  47300  salpreimagtlt  47304  incsmf  47316  decsmf  47341  smflimlem1  47345  smflimlem2  47346  smflimlem3  47347  smflimlem4  47348  smfpimcclem  47381  funressnmo  47640  fcoresf1  47663  aiota0def  47690  euoreqb  47703  2reu8i  47707  2reuimp0  47708  funressndmafv2rn  47817  funressnbrafv2  47838  funbrafv2  47841  smonoord  47971  elsetpreimafvbi  47997  iccpartgt  48033  iccelpart  48039  iccpartiun  48040  icceuelpartlem  48041  icceuelpart  48042  iccpartnel  48044  fargshiftf1  48047  ichexmpl2  48076  ichnreuop  48078  ichreuopeq  48079  sprsymrelfolem2  48099  prproropf1olem4  48112  paireqne  48117  reupr  48128  reuopreuprim  48132  fmtnofac2  48178  fmtnofac1  48179  prmdvdsfmtnof1lem2  48194  perfectALTVlem2  48344  nfermltl8rev  48364  nfermltl2rev  48365  sbgoldbwt  48399  sbgoldbst  48400  sgoldbeven3prm  48405  sbgoldbm  48406  nnsum4primesodd  48418  nnsum4primesoddALTV  48419  evengpop3  48420  evengpoap3  48421  bgoldbnnsum3prm  48426  bgoldbtbndlem4  48430  bgoldbtbnd  48431  tgblthelfgott  48437  tgoldbach  48439  grimuhgr  48509  grimcnv  48510  isuspgrimlem  48517  isubgr3stgrlem4  48591  isubgr3stgrlem6  48593  isubgr3stgrlem7  48594  gpgedg2ov  48688  gpgedg2iv  48689  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgnbgreunbgrlem2lem3  48738  pgnbgreunbgrlem5lem1  48742  pgnbgreunbgrlem5lem2  48743  pgnbgreunbgrlem5lem3  48744  pgnbgreunbgr  48747  ply1mulgsumlem2  49009  islininds  49068  linindslinci  49070  lindslinindsimp1  49079  linds0  49087  lindsrng01  49090  snlindsntorlem  49092  snlindsntor  49093  ldepsnlinc  49130  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  nn0sumshdiglem1  49243  nn0sumshdiglem2  49244  nn0sumshdig  49245  itschlc0yqe  49382  f1mo  49474  iscnrm3lem5  49558  iscnrm3r  49569  isprsd  49576  lubeldm2d  49579  glbeldm2d  49580  joindm2  49589  meetdm2  49591  ipolublem  49607  ipolub  49609  ipoglblem  49610  ipoglb  49612  oppcendc  49639  oppcthinendcALT  50062  functhinclem2  50066  fullthinc  50071  fullthinc2  50072  euendfunc  50147  bnd2d  50302  setrec1lem1  50308  setrec1lem4  50311  setrec2fun  50313