Theorem imbi12d 348

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 345	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 344	. 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  350  ifpbi123d  1080  nfbiit  1858  nfbidv  1930  sbjust  2071  nfbidf  2224  drnf1v  2370  drnf1  2442  mo4  2565  cbvmovw  2601  cbvmow  2602  axextg  2710  cbvabw  2805  nfcriOLD  2887  rspw  3116  ralcom2  3265  raleqbidv  3303  cbvralfw  3334  cbvralfwOLD  3335  cbvralf  3337  cbvralvw  3348  cbvraldva2  3357  vtoclgaf  3478  vtoclga  3479  vtocl2gaf  3481  vtocl3gaf  3482  vtocl3ga  3483  vtocl4ga  3486  rspct  3513  rspc  3515  rspc2gv  3536  rexraleqim  3544  ralab2  3599  ralab2OLD  3600  nelrdva  3607  mob2  3617  mob  3619  morex  3621  reu7  3634  reu8  3635  reu2eqd  3638  cdeqim  3675  sbcimg  3734  csbhypf  3827  cbvralcsf  3843  dfss2f  3877  reldisj  4352  ralidmw  4405  reusngf  4574  rexreusng  4581  reuprg0  4604  elpreqpr  4763  elintab  4856  intss1  4860  intmin  4865  dfiin2g  4927  trel  5153  zfpow  5244  reusv2lem4  5279  reusv3i  5282  rext  5318  opth  5345  copsexgw  5358  copsexg  5359  poeq1  5456  pocl  5460  poclOLD  5461  swopolem  5463  swopo  5464  isso2i  5488  fri  5497  vtoclr  5597  poinxp  5614  posn  5619  ssrel  5639  ssrel2  5641  ssrelrel  5651  relop  5704  reu3op  6135  reuop  6136  predbrg  6160  preddowncl  6168  frpoinsg  6175  wfisg  6183  ordelord  6213  iota5  6341  sbcfung  6382  funopg  6392  brprcneu  6686  fvprc  6687  tz6.12f  6719  funbrfv  6741  ssimaexg  6775  fvmptf  6817  fvelrn  6875  fprg  6948  dff13f  7046  f1veqaeq  7047  fpropnf1  7057  nf1const  7092  soisores  7114  soisoi  7115  isofrlem  7127  isopolem  7132  weniso  7141  riota5f  7177  imbrov2fvoveq  7216  oprabidw  7222  oprabid  7223  f1opr  7245  ovmpos  7335  ov2gf  7336  ov3  7349  caovcan  7390  caovordig  7391  caofrss  7482  caoftrn  7484  tfis  7611  tfisi  7615  tfindsg  7617  tfindsg2  7618  tfindes  7619  dfom2  7624  limomss  7627  nnlim  7636  peano5  7649  findsg  7655  findes  7658  f1oweALT  7723  dfoprab4f  7804  offval22  7834  f1o2ndf1  7869  frxp  7871  poxp  7873  suppfnss  7909  wfrdmcl  8041  onfununi  8056  smoel  8075  smogt  8082  tfrlem1  8090  tz7.48lem  8155  tz7.49  8159  oawordeu  8261  omordi  8272  oeordi  8293  nnmordi  8337  omabs  8354  nneob  8359  omsmolem  8360  qsel  8456  eroveu  8472  ecopovtrn  8480  ixpsnf1o  8597  fundmeng  8687  sbth  8744  limensuc  8801  nneneq  8807  php  8808  php2  8809  findcard  8819  findcard2  8820  findcard2d  8822  pssnn  8824  ssfi  8829  unxpdom  8861  pssnnOLD  8872  findcard2OLD  8891  findcard3  8892  ac6sfi  8893  frfi  8894  domunfican  8922  fiint  8926  iunfi  8942  finsschain  8961  dffi3  9025  marypha1lem  9027  marypha1  9028  supeq3  9043  supeq123d  9044  supmo  9046  suplub  9054  supisolem  9067  eqinf  9078  infval  9080  infmo  9089  ordiso2  9109  ordtypelem7  9118  wemaplem1  9140  wemaplem2  9141  zfregcl  9188  inf0  9214  inf3lem1  9221  zfinf  9232  axinf2  9233  dfom3  9240  elom3  9241  cantnfval2  9262  cantnfle  9264  cantnflt  9265  cantnfp1lem3  9273  oemapvali  9277  cantnflem1c  9280  cantnflem1  9282  cantnf  9286  wemapwe  9290  cnfcom  9293  setind  9328  r1sdom  9355  r1ordg  9359  rankonidlem  9409  rankunb  9431  bnd2  9474  infxpenlem  9592  infxpenc2  9601  dfac8alem  9608  dfac8clem  9611  indcardi  9620  alephordi  9653  alephinit  9674  alephfp  9687  aceq3lem  9699  dfac5lem4  9705  dfac5  9707  dfac2b  9709  dfac9  9715  dfac12lem2  9723  dfac12lem3  9724  kmlem1  9729  kmlem4  9732  kmlem10  9738  kmlem12  9740  kmlem13  9741  pwsdompw  9783  ackbij1lem16  9814  cfslb2n  9847  cfsmolem  9849  sornom  9856  fin2i  9874  infpssrlem4  9885  isfin2-2  9898  isfin3ds  9908  fin23lem17  9917  fin23lem32  9923  fin23lem34  9925  fin23lem35  9926  fin23lem39  9929  fin23lem41  9931  isf32lem2  9933  isf33lem  9945  isf34lem4  9956  isf34lem6  9959  fin1a2lem10  9988  axcc2lem  10015  axcc3  10017  axcc4dom  10020  dominf  10024  axdc2lem  10027  axdc3lem2  10030  ac6sg  10067  zorn2lem7  10081  zornn0g  10084  ttukeylem5  10092  ttukeylem6  10093  axdclem  10098  dominfac  10152  axrepndlem1  10171  axrepndlem2  10172  axunndlem1  10174  axunnd  10175  axpowndlem2  10177  axpowndlem3  10178  axpowndlem4  10179  axregndlem2  10182  axregnd  10183  axinfndlem1  10184  axinfnd  10185  axacndlem4  10189  axacndlem5  10190  axacnd  10191  zfcndpow  10195  zfcndinf  10197  fpwwe2lem4  10213  fpwwe2lem7  10216  fpwwe2lem11  10220  pwfseqlem4a  10240  pwfseqlem4  10241  pwfseqlem5  10242  pwfseq  10243  wunfi  10300  wunex2  10317  inar1  10354  rankcf  10356  tskord  10359  grudomon  10396  grur1a  10398  axgroth6  10407  axgroth3  10410  axgroth4  10411  eltskm  10422  indpi  10486  pinq  10506  nqereu  10508  prcdnq  10572  prnmax  10574  ltsopr  10611  prlem936  10626  ltsosr  10673  recexsrlem  10682  mulgt0sr  10684  map2psrpr  10689  supsrlem  10690  axrrecex  10742  axpre-lttrn  10745  axpre-mulgt0  10747  axpre-sup  10748  axsup  10873  dedekind  10960  ltordlem  11322  ltord1  11323  wloglei  11329  squeeze0  11700  infm3  11756  nnsub  11839  nnunb  12051  peano5uzti  12232  fzind  12240  eluzadd  12434  eluzsub  12435  uzind4s  12469  uzind4s2  12470  zmax  12506  zbtwnre  12507  xmulasslem  12840  xrsupsslem  12862  xrinfmsslem  12863  xrub  12867  infmremnf  12898  injresinj  13328  om2uzlti  13488  uzindi  13520  axdc4uz  13522  ssnn0fi  13523  rabssnn0fi  13524  suppssfz  13532  seqp1  13554  seqcl2  13559  seqfveq2  13563  seqshft2  13567  monoord  13571  seqsplit  13574  seqf1olem2  13581  seqf1o  13582  seqid2  13587  seqhomo  13588  seqof2  13599  expcl2lem  13612  facdiv  13818  facwordi  13820  faclbnd4lem2  13825  hashnn0n0nn  13923  hashf1lem2  13987  seqcoll  13995  fi1uzind  14028  brfi1indALT  14031  wrdind  14252  wrd2ind  14253  swrdccatin1  14255  swrdccat3blem  14269  reuccatpfxs1lem  14276  repswccat  14316  cshf1  14340  trclfvcotr  14537  relexprelg  14566  rtrclreclem4  14589  relexpindlem  14591  ello1mpt  15047  o1co  15112  o1compt  15113  rlimcn3  15116  climcn2  15119  subcn2  15121  o1of2  15139  fsumsplitf  15270  fsum2d  15298  modfsummod  15321  fsumabs  15328  telfsumo  15329  fsumrlim  15338  fsumo1  15339  o1fsum  15340  fsumiun  15348  prodfdiv  15423  fprod2d  15506  fproddivf  15512  fprodsplitf  15513  fprodsplit1f  15515  rpnnen2lem10  15747  sqrt2irr  15773  dvdsle  15834  divalglem7  15923  divalglem8  15924  ndvdssub  15933  gcdcllem1  16021  dfgcd2  16069  algcvg  16096  algcvga  16099  algfx  16100  lcmgcdlem  16126  lcmdvds  16128  lcmf  16153  lcmfunsnlem1  16157  lcmfunsnlem2lem1  16158  lcmfunsnlem  16161  lcmfdvds  16162  lcmfun  16165  coprmgcdb  16169  coprmdvds1  16172  coprmdvds2  16174  coprmprod  16181  coprmproddvds  16183  prmind2  16205  dvdsprime  16207  nprm  16208  dvdsprm  16223  exprmfct  16224  coprm  16231  isprm6  16234  prmfac1  16241  eulerthlem2  16298  pcqmul  16369  pcqcl  16372  pc2dvds  16395  pcz  16397  prmpwdvds  16420  infpn2  16429  vdwlem12  16508  ramub2  16530  rami  16531  ramcl  16545  prmdvdsprmop  16559  prmlem0  16622  mreintcl  17052  ismred2  17060  mrissmrcd  17097  mreexexlemd  17101  iscatd2  17138  moni  17195  yoniso  17747  isprs  17758  prslem  17759  drsdirfi  17766  ispos  17775  posi  17778  isposd  17784  pospropd  17787  lubfval  17810  lublecllem  17820  glbfval  17823  joinle  17846  meetle  17860  poslubmo  17871  posglbmo  17872  lubl  17972  lubun  17975  clatleglb  17978  ipodrsima  18001  acsdrsel  18003  isacs4lem  18004  isacs5lem  18005  acsdrscl  18006  mreclatBAD  18023  pslem  18032  dirtr  18062  mndind  18208  mhmlem  18437  isnsg2  18526  ghmf1  18605  orbsta  18661  symgextf1  18767  gsmsymgrfix  18774  gsmsymgreq  18778  symggen  18816  psgnunilem4  18843  sylow1lem1  18941  sylow2alem2  18961  sylow2a  18962  lsmmod  19019  lsmdisj2  19026  efgsrel  19078  efgredlemd  19088  efgredlem  19091  efgred  19092  gsumzaddlem  19260  gsummptnn0fz  19325  gsummptnn0fzfv  19326  telgsumfzs  19328  telgsums  19332  dprdval  19344  dprddisj2  19380  ablfac1eulem  19413  pgpfac1lem1  19415  pgpfac1lem5  19420  pgpfac1  19421  pgpfaclem2  19423  pgpfac  19425  irredmul  19681  f1rhm0to0ALT  19715  isdrngrd  19747  sdrgacs  19799  islbs3  20146  rrgval  20279  rrgeq0i  20281  isdomn  20286  domneq0  20289  prmirredlem  20413  znfld  20479  znrrg  20484  cygznlem3  20488  isphl  20544  ipeq0  20554  isphld  20570  phlpropd  20571  lsmcss  20608  frlmphl  20697  frlmup1  20714  lindfrn  20737  islindf4  20754  islindf5  20755  mplsubglem  20915  mpllsslem  20916  mplcoe1  20948  mplcoe5  20951  mpfind  21021  ismhp3  21037  coe1fzgsumd  21177  gsummoncoe1  21179  pf1ind  21225  evl1gsumd  21227  dmatelnd  21347  mat1scmat  21390  mdetdiaglem  21449  mdetralt  21459  mdetralt2  21460  mdetunilem1  21463  mdetunilem2  21464  mdetunilem3  21465  mdetunilem4  21466  mdetunilem9  21471  smadiadetr  21526  pmatcoe1fsupp  21552  mp2pm2mplem4  21660  uniopn  21748  fiinopn  21752  epttop  21860  clsndisj  21926  elcls3  21934  neiptoptop  21982  neiptopnei  21983  cnpval  22087  iscnp  22088  cnpimaex  22107  lmcvg  22113  cnprest  22140  cnprest2  22141  lmss  22149  lmff  22152  t0sep  22175  hausnei  22179  isnrm2  22209  t1sep2  22220  isreg2  22228  iscmp  22239  cmpcov  22240  cmpsublem  22250  cmpsub  22251  tgcmp  22252  uncmp  22254  fiuncmp  22255  hauscmplem  22257  cmpfi  22259  cmpfii  22260  dfconn2  22270  connsuba  22271  connsub  22272  nconnsubb  22274  1stcclb  22295  1stcfb  22296  2ndc1stc  22302  1stcrest  22304  1stcelcls  22312  restnlly  22333  lly1stc  22347  comppfsc  22383  kgenval  22386  kgeni  22388  kgencn2  22408  ptcldmpt  22465  ptclsg  22466  dfac14lem  22468  dfac14  22469  txcnp  22471  ptcnp  22473  hausdiag  22496  txlm  22499  tx1stc  22501  xkococn  22511  cnmpt12  22518  cnmpt22  22525  kqt0lem  22587  isr0  22588  regr1lem2  22591  kqreglem1  22592  r0sep  22599  ptcmpfi  22664  elmptrab  22678  isfil  22698  filss  22704  isufil2  22759  cfinufil  22779  rnelfm  22804  fmfnfmlem2  22806  fmfnfmlem4  22808  flimopn  22826  flimrest  22834  flftg  22847  cnpflf  22852  txflf  22857  fclsopni  22866  fclsrest  22875  fclscf  22876  flimfnfcls  22879  fcfnei  22886  alexsublem  22895  alexsubb  22897  alexsubALTlem3  22900  alexsubALTlem4  22901  alexsubALT  22902  cnextcn  22918  cnextfres1  22919  tgpt0  22970  qustgplem  22972  tsmsi  22985  tsmssubm  22994  tsmsres  22995  tsmsf1o  22996  tsmsxp  23006  ustssel  23057  ust0  23071  ustuqtop4  23096  ucnima  23132  ucncn  23136  iscusp  23150  cuspcvg  23152  imasdsf1olem  23225  blssps  23276  blss  23277  metss  23360  comet  23365  metcnp3  23392  metcnp2  23394  txmetcnp  23399  metuel2  23417  metucn  23423  nrmmetd  23426  nlmvscn  23539  nrginvrcn  23544  nmolb  23569  xrge0tsms  23685  divcn  23719  fsumcn  23721  elcncf2  23741  cncfi  23745  mulc1cncf  23756  cncfmet  23760  xrhmeo  23797  bndth  23809  nmoleub2lem2  23967  nmoleub3  23970  ipcn  24097  lmmbr  24109  caucfil  24134  pmltpc  24301  ovolfiniun  24352  ovolicc2lem3  24370  ovolicc2  24373  mblsplit  24383  finiunmbl  24395  volfiniun  24398  voliunlem3  24403  ioorinv  24427  ioorcl  24428  dyadmax  24449  dyadmbllem  24450  dyadmbl  24451  opnmbllem  24452  volcn  24457  vitalilem2  24460  vitalilem3  24461  vitali  24464  i1fd  24532  itg2seq  24594  itg2addlem  24610  itgfsum  24678  ellimc3  24730  dvbsss  24753  dvnres  24782  dvmptfsum  24826  dvferm1lem  24835  dvferm2lem  24837  rolle  24841  c1lip1  24848  lhop1lem  24864  lhop1  24865  dvfsumlem2  24878  dvfsumlem4  24880  dvfsumrlim  24882  dvfsum2  24885  ftc1a  24888  ftc1lem6  24892  mdegleb  24916  mdeglt  24917  deg1leb  24947  deg1lt  24949  ply1divex  24988  fta1glem2  25018  fta1g  25019  plyco0  25040  plyeq0lem  25058  coeeq2  25090  dgrle  25091  dgrcolem2  25122  dgrco  25123  plydivlem4  25143  plydivex  25144  fta1lem  25154  fta1  25155  vieta1lem2  25158  vieta1  25159  aalioulem2  25180  aalioulem4  25182  abelth  25287  cxpcn3  25588  rlimcnp  25802  xrlimcnp  25805  cxploglim  25814  scvxcvx  25822  jensen  25825  lgamgulmlem2  25866  wilthlem2  25905  wilthlem3  25906  fta  25916  dvdsmulf1o  26030  perfectlem2  26065  dchrelbas3  26073  dchrelbas4  26078  dchrn0  26085  bcmono  26112  lgsdir2lem4  26163  lgsdchr  26190  gausslemma2dlem0i  26199  lgseisenlem2  26211  lgsquad2lem2  26220  2sqlem6  26258  2sqlem8  26261  2sqlem10  26263  dchrisumlema  26323  dchrisumlem2  26325  dchrisumlem3  26326  istrkgb  26500  istrkgcb  26501  istrkge  26502  axtgcgrid  26508  axtg5seg  26510  axtgbtwnid  26511  axtgpasch  26512  axtgcont1  26513  axtgeucl  26517  iscgrglt  26559  tgcgr4  26576  axcgrtr  26960  gropd  27076  grstructd  27077  upgredg2vtx  27186  upgredgpr  27187  edglnl  27188  numedglnl  27189  usgredg2vtxeuALT  27264  nbgr2vtx1edg  27392  finsumvtxdg2size  27592  wlkp1lem8  27722  upgrwlkdvdelem  27777  usgr2wlkneq  27797  usgr2pthlem  27804  pthdlem2lem  27808  uspgrn2crct  27846  2pthdlem1  27968  eleclclwwlkn  28113  hashecclwwlkn1  28114  umgrhashecclwwlk  28115  3pthdlem1  28201  eupth2  28276  frgr3vlem1  28310  3vfriswmgrlem  28314  frgrwopreglem4a  28347  frgr2wwlk1  28366  wlkl0  28404  numclwlk2lem2f1o  28416  friendshipgt3  28435  eulplig  28520  nvz  28704  nmobndseqi  28814  nmobndseqiALT  28815  nmlno0  28830  blocnilem  28839  dipdir  28877  dipass  28880  siilem2  28887  ubthlem2  28906  ubth  28908  htth  28953  normpyth  29180  norm3lemt  29187  chlimi  29269  chcompl  29277  omlsii  29438  pjoml  29471  h1de2i  29588  elspansn2  29602  h1datom  29617  pjoml2  29646  pjoml3  29647  lecm  29652  chscllem2  29673  osum  29680  spansncv  29688  pjcjt2  29727  pjopyth  29755  eigre  29870  eigorth  29873  hhcno  29939  hhcnf  29940  cnopc  29948  cnfnc  29965  nmcexi  30061  nmcopexi  30062  nmcfnexi  30086  pjssge0i  30201  hstel2  30254  stj  30270  stri  30292  hstri  30300  stcltr1i  30309  mdbr  30329  mdi  30330  mdbr3  30332  mdbr4  30333  dmdbr  30334  dmdmd  30335  dmdi  30337  dmdbr3  30340  dmdbr4  30341  dmdbr5  30343  mdsl1i  30356  mdslmd1lem3  30362  mdslmd1lem4  30363  mdslmd1i  30364  csmdsymi  30369  cvmd  30371  atss  30381  atom1d  30388  chcv1  30390  hatomic  30395  atord  30423  atcvat2  30424  mddmdin0i  30466  opreu2reuALT  30498  rmoxfrd  30514  ifeqeqx  30558  ssiun2sf  30572  iinabrex  30581  ssrelf  30628  fmptcof2  30668  acunirnmpt  30670  acunirnmpt2  30671  acunirnmpt2f  30672  aciunf1lem  30673  suppovss  30691  fz1nntr  30799  nn0min  30808  fsumiunle  30817  wrdt2ind  30899  ressprs  30914  resspos  30917  toslublem  30923  tosglblem  30925  mntoval  30933  ismntd  30935  dfmgc2lem  30946  dfmgc2  30947  xrge0tsmsd  30990  isomnd  31000  omndadd  31005  gsumle  31023  fzto1st  31043  psgnfzto1st  31045  submarchi  31113  archirng  31115  archiexdiv  31117  archiabllem1a  31118  archiabllem2a  31121  archiabl  31125  gsumvsca1  31152  gsumvsca2  31153  isorng  31171  orngmul  31175  isarchiofld  31189  linds2eq  31243  isprmidl  31281  prmidl  31283  prmidlc  31292  ismxidl  31302  mxidlmax  31305  rprmval  31332  isrprm  31333  lbsdiflsp0  31375  fedgmullem1  31378  fedgmullem2  31379  submateq  31427  lmatfval  31432  lmatcl  31434  iscref  31462  crefi  31465  pcmplfin  31478  xrge0iifiso  31553  esumcvg  31720  esum2dlem  31726  sigaclcu  31751  sigaclci  31766  unelsiga  31768  unelldsys  31792  sigapildsys  31796  ldgenpisyslem1  31797  fiunelros  31808  measvun  31843  measiun  31852  carsgmon  31947  carsgsigalem  31948  carsgclctunlem2  31952  carsgclctun  31954  pmeasmono  31957  pmeasadd  31958  sibfof  31973  sitgclg  31975  eulerpartlemgvv  32009  signsply0  32196  signstfvneq0  32217  breprexp  32279  hgt749d  32295  istrkg2d  32312  axtgupdim2ALTV  32314  bnj1385  32479  bnj110  32505  bnj222  32530  bnj229  32531  bnj590  32557  bnj865  32570  bnj849  32572  bnj981  32597  bnj1014  32608  bnj1015  32609  bnj1112  32630  bnj1118  32631  bnj1123  32633  bnj1128  32637  bnj1125  32639  bnj1148  32643  bnj1154  32646  bnj1326  32673  bnj1384  32679  bnj1489  32703  bnj1497  32707  funen1cnv  32727  f1resfz0f1d  32739  cplgredgex  32749  acycgrcycl  32776  subfacp1lem6  32814  erdszelem9  32828  kur14lem9  32843  sconnpht  32858  cvmsss2  32903  cvmliftlem7  32920  cvmliftlem10  32923  fmlasuc  33015  gonar  33024  goalr  33026  mclsrcl  33190  mclsssvlem  33191  mclsval  33192  mclsax  33198  mclsind  33199  mclsppslem  33212  iota5f  33338  dfpo2  33392  fununiq  33413  setinds  33424  dfon2lem3  33431  dfon2lem4  33432  dfon2lem5  33433  dfon2lem6  33434  dfon2lem7  33435  dfon2lem8  33436  dfon2  33438  tfisg  33456  frpoins3xpg  33457  frpoins3xp3g  33458  frmin  33459  frinsg  33462  poxp2  33470  frxp2  33471  xpord2ind  33474  poxp3  33476  frxp3  33477  xpord3ind  33480  nosupprefixmo  33589  noinfprefixmo  33590  nosupcbv  33591  nosupdm  33593  nosupfv  33595  nosupres  33596  nosupbnd1lem1  33597  nosupbnd1lem3  33599  nosupbnd1lem5  33601  nosupbnd2  33605  noinfcbv  33606  noinfdm  33608  noinffv  33610  noinfres  33611  noinfbnd1lem1  33612  noinfbnd1lem3  33614  noinfbnd1lem5  33616  noinfbnd2  33620  nocvxminlem  33658  madebdaylemold  33764  madebdaylemlrcut  33765  madebday  33766  lrrecpo  33784  btwnconn1lem11  34085  linethru  34141  fwddifnp1  34153  rankelg  34156  rankeq1o  34159  subtr  34189  subtr2  34190  trer  34191  nn0prpwlem  34197  nn0prpw  34198  neibastop2lem  34235  filnetlem4  34256  bj-hbxfrbi  34497  bj-hbyfrbi  34498  bj-ssblem1  34521  bj-ssblem2  34522  bj-ax12  34524  irrdiff  35180  relowlssretop  35220  rdgeqoa  35227  rdgssun  35235  exrecfnlem  35236  finxpreclem6  35253  pibp19  35271  pibt2  35274  wl-mo3t  35417  wl-sb8mot  35419  finixpnum  35448  matunitlindflem1  35459  ptrest  35462  poimirlem13  35476  poimirlem14  35477  poimirlem17  35480  poimirlem18  35481  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem24  35487  poimirlem25  35488  poimirlem26  35489  poimirlem28  35491  poimirlem30  35493  poimirlem31  35494  poimirlem32  35495  poimir  35496  heicant  35498  mblfinlem1  35500  mblfinlem2  35501  mblfinlem3  35502  voliunnfl  35507  volsupnfl  35508  mbfresfi  35509  itg2addnclem3  35516  ftc1cnnc  35535  ftc1anclem7  35542  ftc1anc  35544  sdclem2  35586  fdc  35589  fdc1  35590  neificl  35597  mettrifi  35601  sstotbnd2  35618  cntotbnd  35640  heibor1lem  35653  bfp  35668  isass  35690  ismgmOLD  35694  isexid2  35699  iscringd  35842  ispridl  35878  pridl  35881  ismaxidl  35884  maxidlmax  35887  ispridlc  35914  pridlc  35915  dmnnzd  35919  relcnveq2  36144  ecin0  36170  elrelscnveq2  36297  elsymrels3  36354  eltrrels3  36380  eleqvrels3  36392  eqvrelqsel  36415  axc11n-16  36638  ax12eq  36641  ax12el  36642  ax12inda  36648  ax12v2-o  36649  fsumshftd  36652  riotasv2d  36657  lshpdisj  36687  lsmsatcv  36710  lsat0cv  36733  lcvexchlem4  36737  lcvexchlem5  36738  l1cvpat  36754  isopos  36880  oposlem  36882  isoml  36938  omllaw  36943  isatl  36999  atlex  37016  iscvlat  37023  cvlexch1  37028  glbconN  37077  hlsuprexch  37081  ps-1  37177  3atlem5  37187  psubspi  37447  llnexchb2  37569  elpcliN  37593  pclfinclN  37650  ldilval  37813  ltrnfset  37817  ltrnset  37818  ltrnu  37821  trlfset  37860  trlset  37861  trlval2  37863  cdleme25cv  38058  cdleme31so  38079  cdleme31fv  38090  cdlemefrs29bpre0  38096  cdleme32fva  38137  cdleme40v  38169  trlord  38269  cdlemkid3N  38633  cdlemkid4  38634  dihffval  38930  dihfval  38931  dihval  38932  lpolconN  39187  mapdordlem2  39337  hdmapfval  39527  hdmapval  39528  hdmapval2  39532  sticksstones1  39771  sticksstones2  39772  sticksstones10  39780  sticksstones12a  39782  isdomn4  39835  fsuppind  39930  nnn1suc  39944  ismrcd1  40164  ismrcd2  40165  ismrc  40167  isnacs3  40176  nacsfix  40178  mzpcompact2  40218  fphpd  40282  fphpdo  40283  monotuz  40407  monotoddzzfi  40408  monotoddzz  40409  oddcomabszz  40410  zindbi  40412  setindtrs  40491  dford3lem2  40493  ttac  40502  dnnumch1  40513  fnwe2lem2  40520  aomclem3  40525  aomclem6  40528  aomclem8  40530  dfac11  40531  dfac21  40535  islssfg2  40540  hbtlem5  40597  hbt  40599  flcidc  40643  mendlmod  40662  rababg  40798  elmapintrab  40801  iunrelexpuztr  40945  frege92  41181  frege104  41193  ntrkbimka  41266  ntrk0kbimka  41267  neik0pk1imk0  41275  isotone1  41276  isotone2  41277  ntrclsiso  41295  ntrclskb  41297  ntrneiiso  41319  ntrneik3  41324  ntrneix3  41325  gneispacess2  41374  grur1cld  41464  scottabf  41472  ismnu  41493  mnuop23d  41498  mnuunid  41509  ismnushort  41533  dvgrat  41544  cvgdvgrat  41545  binomcxplemnotnn0  41588  pm14.122b  41655  sbiota1  41666  fnchoice  42186  fiiuncl  42227  iunincfi  42258  disjf1  42334  wessf1ornlem  42336  disjinfi  42345  axccdom  42376  dmrelrnrel  42379  axccd  42382  monoords  42450  fperiodmullem  42456  supxrgere  42486  supxrgelem  42490  supxrge  42491  xrlexaddrp  42505  infxr  42520  infleinf  42525  supxrleubrnmptf  42607  monoordxrv  42638  monoordxr  42639  monoord2xr  42641  fsumclf  42728  fsummulc1f  42729  fsumnncl  42730  fsumsplit1  42731  fsumf1of  42733  fsumreclf  42735  fsumlessf  42736  fsumsermpt  42738  fmul01  42739  fmulcl  42740  fmuldfeqlem1  42741  fmuldfeq  42742  fmul01lt1lem1  42743  fmul01lt1lem2  42744  fprodexp  42753  fprodabs2  42754  fprodcnlem  42758  climmulf  42763  climexp  42764  climsuse  42767  climrecf  42768  climinff  42770  climaddf  42774  mullimc  42775  mullimcf  42782  limcperiod  42787  sumnnodd  42789  lptre2pt  42799  limsupre  42800  neglimc  42806  addlimc  42807  0ellimcdiv  42808  limclner  42810  climsubmpt  42819  climreclf  42823  climeldmeqmpt  42827  climfveqmpt  42830  fnlimfvre  42833  climfveqf  42839  climfveqmpt3  42841  climeldmeqf  42842  limsupref  42844  limsupbnd1f  42845  climeqf  42847  climeldmeqmpt3  42848  climinf2  42866  limsupubuz  42872  climinf2mpt  42873  climinfmpt  42874  limsupmnf  42880  limsupequz  42882  limsupre2  42884  limsupequzmptf  42890  limsupre3  42892  lmbr3  42906  cnrefiisp  42989  xlimxrre  42990  xlimmnfvlem1  42991  xlimpnfvlem1  42995  climxlim2lem  43004  cncfshift  43033  cncfperiod  43038  icccncfext  43046  fprodcncf  43059  fperdvper  43078  dvmptmulf  43096  dvnmptdivc  43097  dvnmul  43102  dvmptfprod  43104  dvnprodlem1  43105  dvnprodlem2  43106  dvnprodlem3  43107  iblspltprt  43132  itgspltprt  43138  stoweidlem3  43162  stoweidlem4  43163  stoweidlem6  43165  stoweidlem8  43167  stoweidlem15  43174  stoweidlem16  43175  stoweidlem17  43176  stoweidlem19  43178  stoweidlem20  43179  stoweidlem22  43181  stoweidlem23  43182  stoweidlem26  43185  stoweidlem27  43186  stoweidlem30  43189  stoweidlem31  43190  stoweidlem32  43191  stoweidlem34  43193  stoweidlem35  43194  stoweidlem42  43201  stoweidlem43  43202  stoweidlem48  43207  stoweidlem50  43209  stoweidlem51  43210  stoweidlem57  43216  stoweidlem59  43218  stoweidlem62  43221  wallispilem3  43226  dirkercncflem2  43263  fourierdlem11  43277  fourierdlem12  43278  fourierdlem15  43281  fourierdlem16  43282  fourierdlem21  43287  fourierdlem34  43300  fourierdlem41  43307  fourierdlem42  43308  fourierdlem46  43311  fourierdlem48  43313  fourierdlem49  43314  fourierdlem50  43315  fourierdlem51  43316  fourierdlem68  43333  fourierdlem71  43336  fourierdlem72  43337  fourierdlem73  43338  fourierdlem76  43341  fourierdlem79  43344  fourierdlem81  43346  fourierdlem83  43348  fourierdlem86  43351  fourierdlem89  43354  fourierdlem90  43355  fourierdlem91  43356  fourierdlem92  43357  fourierdlem94  43359  fourierdlem97  43362  fourierdlem103  43368  fourierdlem104  43369  fourierdlem111  43376  fourierdlem112  43377  fourierdlem113  43378  etransclem2  43395  etransclem46  43439  salunicl  43475  saluncl  43476  intsaluni  43486  dfsalgen2  43498  sge0f1o  43538  sge0lempt  43566  sge0iunmptlemfi  43569  sge0p1  43570  sge0fodjrnlem  43572  sge0iunmpt  43574  sge0ltfirpmpt2  43582  sge0isummpt2  43588  sge0xaddlem2  43590  sge0xadd  43591  nnfoctbdjlem  43611  meadjuni  43613  meadjiun  43622  voliunsge0lem  43628  meaiuninclem  43636  meaiunincf  43639  meaiuninc3v  43640  meaiuninc3  43641  meaiininclem  43642  meaiininc  43643  omeunile  43661  isomenndlem  43686  ovn0lem  43721  ovnsubaddlem1  43726  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  hoidmvle  43756  hspmbllem2  43783  hoimbl2  43821  vonhoire  43828  vonicclem2  43840  vonn0ioo2  43846  vonn0icc2  43848  salpreimagelt  43860  salpreimalegt  43862  pimdecfgtioc  43867  pimincfltioc  43868  pimincfltioo  43870  salpreimagtge  43876  salpreimaltle  43877  salpreimagtlt  43881  incsmf  43893  decsmf  43917  smflimlem1  43921  smflimlem2  43922  smflimlem3  43923  smflimlem4  43924  smfpimcclem  43955  funressnmo  44155  fcoresf1  44178  aiota0def  44203  euoreqb  44216  2reu8i  44220  2reuimp0  44221  funressndmafv2rn  44330  funressnbrafv2  44351  funbrafv2  44354  smonoord  44439  elsetpreimafvbi  44459  iccpartgt  44495  iccelpart  44501  iccpartiun  44502  icceuelpartlem  44503  icceuelpart  44504  iccpartnel  44506  fargshiftf1  44509  ichexmpl2  44538  ichnreuop  44540  ichreuopeq  44541  sprsymrelfolem2  44561  prproropf1olem4  44574  paireqne  44579  reupr  44590  reuopreuprim  44594  fmtnofac2  44637  fmtnofac1  44638  prmdvdsfmtnof1lem2  44653  perfectALTVlem2  44790  nfermltl8rev  44810  nfermltl2rev  44811  sbgoldbwt  44845  sbgoldbst  44846  sgoldbeven3prm  44851  sbgoldbm  44852  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  evengpop3  44866  evengpoap3  44867  bgoldbnnsum3prm  44872  bgoldbtbndlem4  44876  bgoldbtbnd  44877  tgblthelfgott  44883  tgoldbach  44885  isomuspgrlem2b  44897  ply1mulgsumlem2  45344  islininds  45403  linindslinci  45405  lindslinindsimp1  45414  linds0  45422  lindsrng01  45425  snlindsntorlem  45427  snlindsntor  45428  ldepsnlinc  45465  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582  nn0sumshdiglem1  45583  nn0sumshdiglem2  45584  nn0sumshdig  45585  itschlc0yqe  45722  f1mo  45796  iscnrm3lem5  45847  iscnrm3r  45858  isprsd  45865  lubeldm2d  45868  glbeldm2d  45869  joindm2  45878  meetdm2  45880  ipolublem  45888  ipolub  45890  ipoglblem  45891  ipoglb  45893  functhinclem2  45939  fullthinc  45943  fullthinc2  45944  bnd2d  46001  setrec1lem1  46007  setrec1lem4  46010  setrec2fun  46012