Theorem imbi12d 335

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  imbi12  337  nfbiit  1936  nfbidv  2013  nfbidf  2260  nfbidfOLD  2375  axc15  2471  drnf1  2491  mobidv  2637  mobid  2651  axext3ALT  2787  ralcom2  3292  cbvralf  3354  cbvraldva2  3364  vtoclgaf  3464  vtocl2gaf  3466  vtocl3gaf  3468  vtocl4ga  3471  rspct  3495  rspc  3496  rspc2gv  3514  rexraleqim  3522  ralab2  3567  mob2  3584  mob  3586  morex  3588  reu7  3599  reu8  3600  reu2eqd  3601  nelrdva  3615  cdeqim  3626  sbcimg  3675  csbhypf  3747  cbvralcsf  3760  dfss2f  3789  prel12gOLD  4574  elpreqpr  4589  elintab  4680  intss1  4684  intmin  4689  dfiin2g  4745  trel  4953  zfpow  5036  reusv2lem4  5070  reusv3i  5073  rext  5106  opth  5134  copsexg  5145  poeq1  5235  pocl  5239  swopolem  5241  swopo  5242  isso2i  5264  fri  5273  vtoclr  5364  poinxp  5384  posn  5389  ssrel  5409  ssrelOLD  5410  ssrel2  5412  ssrelrel  5422  relop  5474  idrefOLD  5720  predbrg  5913  preddowncl  5920  wfisg  5928  ordelord  5958  iota5  6084  sbcfung  6125  funopg  6135  brprcneu  6400  tz6.12f  6432  funbrfv  6454  ssimaexg  6485  fvmptf  6522  fvelrn  6574  fprg  6646  dff13f  6737  f1veqaeq  6738  fpropnf1  6748  soisores  6801  soisoi  6802  isofrlem  6814  isopolem  6819  weniso  6828  riota5f  6860  imbrov2fvoveq  6899  oprabid  6905  ovmpt2s  7014  ov2gf  7015  ov3  7027  caovcan  7068  caovordig  7069  caofrss  7160  caoftrn  7162  tfis  7284  tfisi  7288  tfindsg  7290  tfindsg2  7291  tfindes  7292  dfom2  7297  limomss  7300  nnlim  7308  findsg  7323  findes  7326  f1oweALT  7382  dfoprab4f  7458  offval22  7487  f1o2ndf1  7519  frxp  7521  poxp  7523  suppfnss  7554  suppfnssOLD  7555  wfrdmcl  7659  onfununi  7674  smoel  7693  smogt  7700  tfrlem1  7708  tz7.48lem  7772  tz7.49  7776  oawordeu  7872  omordi  7883  oeordi  7904  nnmordi  7948  omabs  7964  nneob  7969  omsmolem  7970  qsel  8061  eroveu  8078  ecopovtrn  8086  ixpsnf1o  8185  fundmeng  8267  sbth  8319  limensuc  8376  nneneq  8382  php  8383  php2  8384  unxpdom  8406  pssnn  8417  findcard  8438  findcard2  8439  findcard2d  8441  findcard3  8442  ac6sfi  8443  frfi  8444  domunfican  8472  fiint  8476  iunfi  8493  finsschain  8512  dffi3  8576  marypha1lem  8578  marypha1  8579  supeq3  8594  supeq123d  8595  supmo  8597  suplub  8605  supisolem  8618  eqinf  8629  infval  8631  infmo  8640  ordiso2  8659  ordtypelem7  8668  wemaplem1  8690  wemaplem2  8691  zfregcl  8738  inf0  8765  inf3lem1  8772  zfinf  8783  axinf2  8784  dfom3  8791  elom3  8792  cantnfval2  8813  cantnfle  8815  cantnflt  8816  cantnfp1lem3  8824  oemapvali  8828  cantnflem1c  8831  cantnflem1  8833  cantnf  8837  wemapwe  8841  cnfcom  8844  setind  8857  r1sdom  8884  r1ordg  8888  rankonidlem  8938  rankunb  8960  bnd2  9003  infxpenlem  9119  infxpenc2  9128  dfac8alem  9135  dfac8clem  9138  indcardi  9147  alephordi  9180  alephinit  9201  alephfp  9214  aceq3lem  9226  dfac5lem4  9232  dfac5  9234  dfac2b  9236  dfac2OLD  9238  dfac9  9243  dfac12lem2  9251  dfac12lem3  9252  kmlem1  9257  kmlem4  9260  kmlem10  9266  kmlem12  9268  kmlem13  9269  pwsdompw  9311  ackbij1lem16  9342  cfslb2n  9375  cfsmolem  9377  sornom  9384  fin2i  9402  infpssrlem4  9413  isfin2-2  9426  isfin3ds  9436  fin23lem17  9445  fin23lem32  9451  fin23lem34  9453  fin23lem35  9454  fin23lem39  9457  fin23lem41  9459  isf32lem2  9461  isf33lem  9473  isf34lem4  9484  isf34lem6  9487  fin1a2lem10  9516  axcc2lem  9543  axcc3  9545  axcc4dom  9548  dominf  9552  axdc2lem  9555  axdc3lem2  9558  ac6sg  9595  zorn2lem7  9609  zornn0g  9612  ttukeylem5  9620  ttukeylem6  9621  axdclem  9626  fodomg  9630  dominfac  9680  axrepndlem1  9699  axrepndlem2  9700  axunndlem1  9702  axunnd  9703  axpowndlem2  9705  axpowndlem3  9706  axpowndlem4  9707  axregndlem2  9710  axregnd  9711  axinfndlem1  9712  axinfnd  9713  axacndlem4  9717  axacndlem5  9718  axacnd  9719  zfcndpow  9723  zfcndinf  9725  fpwwe2lem5  9741  fpwwe2lem8  9744  fpwwe2lem12  9748  pwfseqlem4a  9768  pwfseqlem4  9769  pwfseqlem5  9770  pwfseq  9771  wunfi  9828  wunex2  9845  inar1  9882  rankcf  9884  tskord  9887  grudomon  9924  grur1a  9926  axgroth6  9935  axgroth3  9938  axgroth4  9939  eltskm  9950  indpi  10014  pinq  10034  nqereu  10036  prcdnq  10100  prnmax  10102  ltsopr  10139  prlem936  10154  ltsosr  10200  recexsrlem  10209  mulgt0sr  10211  map2psrpr  10216  supsrlem  10217  axrrecex  10269  axpre-lttrn  10272  axpre-mulgt0  10274  axpre-sup  10275  axsup  10398  dedekind  10485  ltordlem  10838  ltord1  10839  wloglei  10845  squeeze0  11211  infm3  11267  nnsub  11345  nnunb  11555  peano5uzti  11733  fzind  11741  eluzadd  11933  eluzsub  11934  uzind4s  11966  uzind4s2  11967  zmax  12004  zbtwnre  12005  xmulasslem  12333  xrsupsslem  12355  xrinfmsslem  12356  xrub  12360  infmremnf  12391  injresinj  12813  om2uzlti  12973  uzindi  13005  axdc4uz  13007  ssnn0fi  13008  rabssnn0fi  13009  suppssfz  13017  seqp1  13039  seqcl2  13042  seqfveq2  13046  seqshft2  13050  monoord  13054  seqsplit  13057  seqf1olem2  13064  seqf1o  13065  seqid2  13070  seqhomo  13071  seqof2  13082  expcl2lem  13095  facdiv  13294  facwordi  13296  faclbnd4lem2  13301  hashnn0n0nn  13398  hashf1lem2  13457  seqcoll  13465  fi1uzind  13496  brfi1indALT  13499  wrdind  13700  wrd2ind  13701  reuccats1lem  13703  swrdccatin1  13707  swrdccat3blem  13719  repswccat  13756  cshf1  13780  trclfvcotr  13973  relexprelg  14001  rtrclreclem4  14024  relexpindlem  14026  ello1mpt  14475  o1co  14540  o1compt  14541  rlimcn2  14544  climcn2  14546  subcn2  14548  o1of2  14566  fsumsplitf  14695  fsum2d  14725  modfsummod  14748  fsumabs  14755  telfsumo  14756  fsumrlim  14765  fsumo1  14766  o1fsum  14767  fsumiun  14775  prodfdiv  14849  fprod2d  14932  fproddivf  14938  fprodsplitf  14939  fprodsplit1f  14941  rpnnen2lem10  15172  sqrt2irr  15199  dvdsle  15255  divalglem7  15342  divalglem8  15343  ndvdssub  15352  gcdcllem1  15440  dfgcd2  15482  algcvg  15508  algcvga  15511  algfx  15512  lcmgcdlem  15538  lcmdvds  15540  lcmf  15565  lcmfunsnlem1  15569  lcmfunsnlem2lem1  15570  lcmfunsnlem  15573  lcmfdvds  15574  lcmfun  15577  coprmgcdb  15581  coprmdvds1  15584  coprmdvds2  15586  coprmprod  15593  coprmproddvds  15595  prmind2  15616  dvdsprime  15618  nprm  15619  dvdsprm  15632  exprmfct  15633  coprm  15640  isprm6  15643  prmfac1  15648  eulerthlem2  15704  pcqmul  15775  pcqcl  15778  pc2dvds  15800  pcz  15802  prmpwdvds  15825  infpn2  15834  vdwlem12  15913  ramub2  15935  rami  15936  ramcl  15950  prmdvdsprmop  15964  prmlem0  16024  mreintcl  16460  ismred2  16468  mrissmrcd  16505  mreexexlemd  16509  iscatd2  16546  moni  16600  yoniso  17130  isprs  17135  prslem  17136  drsdirfi  17143  ispos  17152  posi  17155  isposd  17160  lubfval  17183  lublecllem  17193  glbfval  17196  joinle  17219  meetle  17233  lubl  17325  lubun  17328  clatleglb  17331  pospropd  17339  poslubmo  17351  posglbmo  17352  ipodrsima  17370  acsdrsel  17372  isacs4lem  17373  isacs5lem  17374  acsdrscl  17375  mreclatBAD  17392  pslem  17411  dirtr  17441  mrcmndind  17571  mhmlem  17740  isnsg2  17826  ghmf1  17891  orbsta  17947  symgextf1  18042  gsmsymgrfix  18049  gsmsymgreq  18053  symggen  18091  psgnunilem4  18118  sylow1lem1  18214  sylow2alem2  18234  sylow2a  18235  lsmmod  18289  lsmdisj2  18296  efgsrel  18348  efgredlemd  18358  efgredlem  18361  efgred  18362  gsumzaddlem  18522  gsummptnn0fz  18583  gsummptnn0fzOLD  18584  gsummptnn0fzfv  18586  telgsumfzs  18588  telgsums  18592  dprdval  18604  dprddisj2  18640  ablfac1eulem  18673  pgpfac1lem1  18675  pgpfac1lem5  18680  pgpfac1  18681  pgpfaclem2  18683  pgpfac  18685  irredmul  18911  f1rhm0to0ALT  18945  isdrngrd  18977  islbs3  19364  rrgval  19496  rrgeq0i  19498  isdomn  19503  domneq0  19506  mplsubglem  19643  mpllsslem  19644  mplcoe1  19674  mplcoe5  19677  mpfind  19744  coe1fzgsumd  19880  gsummoncoe1  19882  pf1ind  19927  evl1gsumd  19929  prmirredlem  20049  znfld  20116  znrrg  20121  cygznlem3  20125  isphl  20183  ipeq0  20193  isphld  20209  phlpropd  20210  lsmcss  20246  frlmphl  20330  frlmup1  20347  lindfrn  20370  islindf4  20387  islindf5  20388  dmatelnd  20513  mat1scmat  20556  mdetdiaglem  20615  mdetralt  20625  mdetralt2  20626  mdetunilem1  20629  mdetunilem2  20630  mdetunilem3  20631  mdetunilem4  20632  mdetunilem9  20637  smadiadetr  20693  pmatcoe1fsupp  20719  mp2pm2mplem4  20827  uniopn  20915  fiinopn  20919  epttop  21027  clsndisj  21093  elcls3  21101  neiptoptop  21149  neiptopnei  21150  cnpval  21254  iscnp  21255  cnpimaex  21274  lmcvg  21280  cnprest  21307  cnprest2  21308  lmss  21316  lmff  21319  ist1  21339  t0sep  21342  hausnei  21346  isnrm2  21376  t1sep2  21387  isreg2  21395  iscmp  21405  cmpcov  21406  cmpsublem  21416  cmpsub  21417  tgcmp  21418  uncmp  21420  fiuncmp  21421  hauscmplem  21423  cmpfi  21425  cmpfii  21426  dfconn2  21436  connsuba  21437  connsub  21438  nconnsubb  21440  1stcclb  21461  1stcfb  21462  2ndc1stc  21468  1stcrest  21470  1stcelcls  21478  restnlly  21499  lly1stc  21513  comppfsc  21549  kgenval  21552  kgeni  21554  kgencn2  21574  ptcldmpt  21631  ptclsg  21632  dfac14lem  21634  dfac14  21635  txcnp  21637  ptcnp  21639  hausdiag  21662  txlm  21665  tx1stc  21667  xkococn  21677  cnmpt12  21684  cnmpt22  21691  kqt0lem  21753  isr0  21754  regr1lem2  21757  kqreglem1  21758  r0sep  21765  ptcmpfi  21830  elmptrab  21844  isfil  21864  filss  21870  isufil2  21925  cfinufil  21945  rnelfm  21970  fmfnfmlem2  21972  fmfnfmlem4  21974  flimopn  21992  flimrest  22000  flftg  22013  cnpflf  22018  txflf  22023  fclsopni  22032  fclsrest  22041  fclscf  22042  flimfnfcls  22045  fcfnei  22052  alexsublem  22061  alexsubb  22063  alexsubALTlem3  22066  alexsubALTlem4  22067  alexsubALT  22068  cnextcn  22084  cnextfres1  22085  tgpt0  22135  qustgplem  22137  tsmsi  22150  tsmssubm  22159  tsmsres  22160  tsmsf1o  22161  tsmsxp  22171  ustssel  22222  ust0  22236  ustuqtop4  22261  ucnima  22298  ucncn  22302  iscusp  22316  cuspcvg  22318  imasdsf1olem  22391  blssps  22442  blss  22443  metss  22526  comet  22531  metcnp3  22558  metcnp2  22560  txmetcnp  22565  metuel2  22583  metucn  22589  nrmmetd  22592  nlmvscn  22704  nrginvrcn  22709  nmolb  22734  xrge0tsms  22850  divcn  22884  fsumcn  22886  elcncf2  22906  cncfi  22910  mulc1cncf  22921  cncfmet  22924  xrhmeo  22958  bndth  22970  nmoleub2lem2  23128  nmoleub3  23131  ipcn  23257  lmmbr  23268  caucfil  23293  pmltpc  23431  ovolfiniun  23482  ovolicc2lem3  23500  ovolicc2  23503  mblsplit  23513  finiunmbl  23525  volfiniun  23528  voliunlem3  23533  ioorinv  23557  ioorcl  23558  dyadmax  23579  dyadmbllem  23580  dyadmbl  23581  opnmbllem  23582  volcn  23587  vitalilem2  23590  vitalilem3  23591  vitali  23594  i1fd  23662  itg2seq  23723  itg2addlem  23739  itgfsum  23807  ellimc3  23857  dvbsss  23880  dvnres  23908  dvmptfsum  23952  dvferm1lem  23961  dvferm2lem  23963  rolle  23967  c1lip1  23974  lhop1lem  23990  lhop1  23991  dvfsumlem2  24004  dvfsumlem4  24006  dvfsumrlim  24008  dvfsum2  24011  ftc1a  24014  ftc1lem6  24018  mdegleb  24038  mdeglt  24039  deg1leb  24069  deg1lt  24071  ply1divex  24110  fta1glem2  24140  fta1g  24141  plyco0  24162  plyeq0lem  24180  coeeq2  24212  dgrle  24213  dgrcolem2  24244  dgrco  24245  plydivlem4  24265  plydivex  24266  fta1lem  24276  fta1  24277  vieta1lem2  24280  vieta1  24281  aalioulem2  24302  aalioulem4  24304  abelth  24409  cxpcn3  24703  rlimcnp  24906  xrlimcnp  24909  cxploglim  24918  scvxcvx  24926  jensen  24929  lgamgulmlem2  24970  wilthlem2  25009  wilthlem3  25010  fta  25020  dvdsmulf1o  25134  perfectlem2  25169  dchrelbas3  25177  dchrelbas4  25182  dchrn0  25189  bcmono  25216  lgsdir2lem4  25267  lgsdchr  25294  gausslemma2dlem0i  25303  lgseisenlem2  25315  lgsquad2lem2  25324  2sqlem6  25362  2sqlem8  25365  2sqlem10  25367  dchrisumlema  25391  dchrisumlem2  25393  dchrisumlem3  25394  istrkgb  25568  istrkgcb  25569  istrkge  25570  axtgcgrid  25576  axtg5seg  25578  axtgbtwnid  25579  axtgpasch  25580  axtgcont1  25581  axtgeucl  25585  iscgrglt  25623  tgcgr4  25640  axcgrtr  26009  gropd  26137  grstructd  26138  upgredg2vtx  26251  upgredgpr  26252  edglnl  26253  numedglnl  26254  usgredg2vtxeuALT  26329  nbgr2vtx1edg  26462  finsumvtxdg2size  26674  wlkp1lem8  26805  upgrwlkdvdelem  26860  usgr2wlkneq  26880  usgr2pthlem  26887  pthdlem2lem  26891  uspgrn2crct  26929  2pthdlem1  27070  eleclclwwlkn  27227  hashecclwwlkn1  27228  umgrhashecclwwlk  27229  3pthdlem1  27337  eupth2  27412  frgr3vlem1  27448  3vfriswmgrlem  27452  frgrwopreglem4a  27485  frgr2wwlk1  27504  wlkl0  27547  numclwlk2lem2f1o  27559  numclwlk2lem2f1oOLD  27566  friendshipgt3  27586  eulplig  27668  nvz  27852  nmobndseqi  27962  nmobndseqiALT  27963  nmlno0  27978  blocnilem  27987  dipdir  28025  dipass  28028  siilem2  28035  ubthlem2  28055  ubth  28057  htth  28103  normpyth  28330  norm3lemt  28337  chlimi  28419  chcompl  28427  omlsii  28590  pjoml  28623  h1de2i  28740  elspansn2  28754  h1datom  28769  pjoml2  28798  pjoml3  28799  lecm  28804  chscllem2  28825  osum  28832  spansncv  28840  pjcjt2  28879  pjopyth  28907  eigre  29022  eigorth  29025  hhcno  29091  hhcnf  29092  cnopc  29100  cnfnc  29117  nmcexi  29213  nmcopexi  29214  nmcfnexi  29238  pjssge0i  29353  hstel2  29406  stj  29422  stri  29444  hstri  29452  stcltr1i  29461  mdbr  29481  mdi  29482  mdbr3  29484  mdbr4  29485  dmdbr  29486  dmdmd  29487  dmdi  29489  dmdbr3  29492  dmdbr4  29493  dmdbr5  29495  mdsl1i  29508  mdslmd1lem3  29514  mdslmd1lem4  29515  mdslmd1i  29516  csmdsymi  29521  cvmd  29523  atss  29533  atom1d  29540  chcv1  29542  hatomic  29547  atord  29575  atcvat2  29576  mddmdin0i  29618  rmoxfrdOLD  29658  rmoxfrd  29659  ifeqeqx  29686  ssiun2sf  29703  ssrelf  29752  fmptcof2  29784  acunirnmpt  29786  acunirnmpt2  29787  acunirnmpt2f  29788  aciunf1lem  29789  fz1nntr  29888  nn0min  29894  fsumiunle  29902  ressprs  29980  resspos  29984  toslublem  29992  tosglblem  29994  isomnd  30026  omndadd  30031  submarchi  30065  archirng  30067  archiexdiv  30069  archiabllem1a  30070  archiabllem2a  30073  archiabl  30077  gsumle  30104  gsumvsca1  30107  gsumvsca2  30108  xrge0tsmsd  30110  isorng  30124  orngmul  30128  isarchiofld  30142  fzto1st  30178  psgnfzto1st  30180  submateq  30200  lmatfval  30205  lmatcl  30207  iscref  30236  crefi  30239  pcmplfin  30252  xrge0iifiso  30306  esumcvg  30473  esum2dlem  30479  isrnsigaOLD  30500  sigaclcu  30505  sigaclci  30520  unelsiga  30522  unelldsys  30546  sigapildsys  30550  ldgenpisyslem1  30551  fiunelros  30562  measvun  30597  measiun  30606  carsgmon  30701  carsgsigalem  30702  carsgclctunlem2  30706  carsgclctun  30708  pmeasmono  30711  pmeasadd  30712  sibfof  30727  sitgclg  30729  eulerpartlemgvv  30763  signsply0  30953  signstfvneq0  30974  breprexp  31036  hgt749d  31052  istrkg2d  31069  axtgupdim2OLD  31071  bnj1385  31226  bnj110  31251  bnj222  31276  bnj229  31277  bnj590  31303  bnj865  31316  bnj849  31318  bnj981  31343  bnj1014  31353  bnj1015  31354  bnj1112  31374  bnj1118  31375  bnj1123  31377  bnj1128  31381  bnj1125  31383  bnj1148  31387  bnj1154  31390  bnj1326  31417  bnj1384  31423  bnj1489  31447  bnj1497  31451  subfacp1lem6  31490  erdszelem9  31504  kur14lem9  31519  sconnpht  31534  cvmsss2  31579  cvmliftlem7  31596  cvmliftlem10  31599  mclsrcl  31781  mclsssvlem  31782  mclsval  31783  mclsax  31789  mclsind  31790  mclsppslem  31803  iota5f  31928  dfpo2  31967  fununiq  31989  setinds  32003  dfon2lem3  32010  dfon2lem4  32011  dfon2lem5  32012  dfon2lem6  32013  dfon2lem7  32014  dfon2lem8  32015  dfon2  32017  tfisg  32036  frpoinsg  32062  frmin  32063  frinsg  32066  frrlem5e  32109  noprefixmo  32169  nosupdm  32171  nosupfv  32173  nosupres  32174  nosupbnd1lem1  32175  nosupbnd1lem3  32177  nosupbnd1lem5  32179  nosupbnd2  32183  nocvxminlem  32214  btwnconn1lem11  32525  linethru  32581  fwddifnp1  32593  rankelg  32596  rankeq1o  32599  subtr  32629  subtr2  32630  trer  32631  nn0prpwlem  32638  nn0prpw  32639  neibastop2lem  32676  filnetlem4  32697  bj-hbxfrbi  32923  bj-ssbjust  32934  bj-ssblem1  32946  bj-ssblem2  32947  bj-drnf1v  33064  bj-axext3  33083  bj-zfpow  33109  relowlssretop  33527  rdgeqoa  33534  finxpreclem6  33549  wl-mo3t  33672  wl-sb8mot  33674  finixpnum  33707  matunitlindflem1  33718  ptrest  33721  poimirlem13  33735  poimirlem14  33736  poimirlem17  33739  poimirlem18  33740  poimirlem20  33742  poimirlem21  33743  poimirlem22  33744  poimirlem24  33746  poimirlem25  33747  poimirlem26  33748  poimirlem28  33750  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  poimir  33755  heicant  33757  mblfinlem1  33759  mblfinlem2  33760  mblfinlem3  33761  voliunnfl  33766  volsupnfl  33767  mbfresfi  33768  itg2addnclem3  33775  ftc1cnnc  33796  ftc1anclem7  33803  ftc1anc  33805  f1opr  33831  sdclem2  33849  fdc  33852  fdc1  33853  neificl  33860  mettrifi  33864  sstotbnd2  33884  cntotbnd  33906  heibor1lem  33919  bfp  33934  isass  33956  ismgmOLD  33960  isexid2  33965  iscringd  34108  ispridl  34144  pridl  34147  ismaxidl  34150  maxidlmax  34153  ispridlc  34180  pridlc  34181  dmnnzd  34185  relcnveq2  34409  ecin0  34430  elrelscnveq2  34556  elsymrels3  34613  axc11n-16  34717  ax12eq  34720  ax12el  34721  ax12inda  34727  ax12v2-o  34728  fsumshftd  34731  riotasv2d  34736  lshpdisj  34767  lsmsatcv  34790  lsat0cv  34813  lcvexchlem4  34817  lcvexchlem5  34818  l1cvpat  34834  isopos  34960  oposlem  34962  isoml  35018  omllaw  35023  isatl  35079  atlex  35096  iscvlat  35103  cvlexch1  35108  glbconN  35157  hlsuprexch  35161  ps-1  35257  3atlem5  35267  psubspi  35527  llnexchb2  35649  elpcliN  35673  pclfinclN  35730  ldilval  35893  ltrnfset  35897  ltrnset  35898  ltrnu  35901  trlfset  35941  trlset  35942  trlval2  35944  cdleme25cv  36139  cdleme31so  36160  cdleme31fv  36171  cdlemefrs29bpre0  36177  cdleme32fva  36218  cdleme40v  36250  trlord  36350  cdlemkid3N  36714  cdlemkid4  36715  dihffval  37011  dihfval  37012  dihval  37013  lpolconN  37268  mapdordlem2  37418  hdmapfval  37608  hdmapval  37609  hdmapval2  37613  ismrcd1  37763  ismrcd2  37764  ismrc  37766  isnacs3  37775  nacsfix  37777  mzpcompact2  37817  fphpd  37882  fphpdo  37883  monotuz  38007  monotoddzzfi  38008  monotoddzz  38009  oddcomabszz  38010  zindbi  38012  setindtrs  38093  dford3lem2  38095  ttac  38104  dnnumch1  38115  fnwe2lem2  38122  aomclem3  38127  aomclem6  38130  aomclem8  38132  dfac11  38133  dfac21  38137  islssfg2  38142  hbtlem5  38199  hbt  38201  flcidc  38245  mendlmod  38264  sdrgacs  38272  ifpbi123  38335  rababg  38379  elmapintrab  38382  iunrelexpuztr  38511  frege92  38749  frege104  38761  ntrkbimka  38836  ntrk0kbimka  38837  neik0pk1imk0  38845  isotone1  38846  isotone2  38847  ntrclsiso  38865  ntrclskb  38867  ntrneiiso  38889  ntrneik3  38894  ntrneix3  38895  gneispacess2  38944  dvgrat  39011  cvgdvgrat  39012  binomcxplemnotnn0  39055  pm14.122b  39123  sbiota1  39134  sbcssOLD  39254  fnchoice  39682  fiiuncl  39727  iunincfi  39765  disjf1  39858  wessf1ornlem  39860  disjinfi  39869  axccdom  39903  dmrelrnrel  39906  axccd  39913  monoords  39992  fperiodmullem  39998  supxrgere  40029  supxrgelem  40033  supxrge  40034  xrlexaddrp  40048  infxr  40063  infleinf  40068  supxrleubrnmptf  40159  monoordxrv  40191  monoordxr  40192  monoord2xr  40194  fsumclf  40281  fsummulc1f  40282  fsumnncl  40283  fsumsplit1  40284  fsumf1of  40286  fsumreclf  40288  fsumlessf  40289  fsumsermpt  40291  fmul01  40292  fmulcl  40293  fmuldfeqlem1  40294  fmuldfeq  40295  fmul01lt1lem1  40296  fmul01lt1lem2  40297  fprodexp  40306  fprodabs2  40307  fprodcnlem  40311  climmulf  40316  climexp  40317  climsuse  40320  climrecf  40321  climinff  40323  climaddf  40327  mullimc  40328  mullimcf  40335  limcperiod  40340  sumnnodd  40342  lptre2pt  40352  limsupre  40353  neglimc  40359  addlimc  40360  0ellimcdiv  40361  limclner  40363  climsubmpt  40372  climreclf  40376  climeldmeqmpt  40380  climfveqmpt  40383  fnlimfvre  40386  climfveqf  40392  climfveqmpt3  40394  climeldmeqf  40395  limsupref  40397  limsupbnd1f  40398  climeqf  40400  climeldmeqmpt3  40401  climinf2  40419  limsupubuz  40425  climinf2mpt  40426  climinfmpt  40427  limsupmnf  40433  limsupequz  40435  limsupre2  40437  limsupequzmptf  40443  limsupre3  40445  lmbr3  40459  cnrefiisp  40536  xlimxrre  40537  xlimmnfvlem1  40538  xlimpnfvlem1  40542  climxlim2lem  40551  cncfshift  40567  cncfperiod  40572  icccncfext  40580  cncfiooicclem1  40586  fprodcncf  40594  fperdvper  40613  dvmptmulf  40632  dvnmptdivc  40633  dvnmul  40638  dvmptfprod  40640  dvnprodlem1  40641  dvnprodlem2  40642  dvnprodlem3  40643  iblspltprt  40668  itgspltprt  40674  stoweidlem3  40699  stoweidlem4  40700  stoweidlem6  40702  stoweidlem8  40704  stoweidlem15  40711  stoweidlem16  40712  stoweidlem17  40713  stoweidlem19  40715  stoweidlem20  40716  stoweidlem22  40718  stoweidlem23  40719  stoweidlem26  40722  stoweidlem27  40723  stoweidlem30  40726  stoweidlem31  40727  stoweidlem32  40728  stoweidlem34  40730  stoweidlem35  40731  stoweidlem42  40738  stoweidlem43  40739  stoweidlem48  40744  stoweidlem50  40746  stoweidlem51  40747  stoweidlem57  40753  stoweidlem59  40755  stoweidlem62  40758  wallispilem3  40763  dirkercncflem2  40800  fourierdlem11  40814  fourierdlem12  40815  fourierdlem15  40818  fourierdlem16  40819  fourierdlem21  40824  fourierdlem34  40837  fourierdlem41  40844  fourierdlem42  40845  fourierdlem46  40848  fourierdlem48  40850  fourierdlem49  40851  fourierdlem50  40852  fourierdlem51  40853  fourierdlem68  40870  fourierdlem71  40873  fourierdlem72  40874  fourierdlem73  40875  fourierdlem76  40878  fourierdlem79  40881  fourierdlem81  40883  fourierdlem83  40885  fourierdlem86  40888  fourierdlem89  40891  fourierdlem90  40892  fourierdlem91  40893  fourierdlem92  40894  fourierdlem94  40896  fourierdlem97  40899  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  fourierdlem112  40914  fourierdlem113  40915  etransclem2  40932  etransclem46  40976  salunicl  41015  saluncl  41016  intsaluni  41026  dfsalgen2  41038  sge0f1o  41078  sge0lempt  41106  sge0iunmptlemfi  41109  sge0p1  41110  sge0fodjrnlem  41112  sge0iunmpt  41114  sge0ltfirpmpt2  41122  sge0isummpt2  41128  sge0xaddlem2  41130  sge0xadd  41131  nnfoctbdjlem  41151  meadjuni  41153  meadjiun  41162  voliunsge0lem  41168  meaiuninclem  41176  meaiunincf  41179  meaiuninc3v  41180  meaiuninc3  41181  meaiininclem  41182  meaiininc  41183  omeunile  41201  isomenndlem  41226  ovn0lem  41261  ovnsubaddlem1  41266  hoidmvlelem2  41292  hoidmvlelem3  41293  hoidmvlelem4  41294  hoidmvle  41296  hspmbllem2  41323  hoimbl2  41361  vonhoire  41368  vonicclem2  41380  vonn0ioo2  41386  vonn0icc2  41388  salpreimagelt  41400  salpreimalegt  41402  pimdecfgtioc  41407  pimincfltioc  41408  pimincfltioo  41410  salpreimagtge  41416  salpreimaltle  41417  salpreimagtlt  41421  incsmf  41433  decsmf  41457  smflimlem1  41461  smflimlem2  41462  smflimlem3  41463  smflimlem4  41464  smfpimcclem  41495  funressnmo  41665  aiota0def  41678  funressndmafv2rn  41812  funressnbrafv2  41833  funbrafv2  41836  smonoord  41916  iccpartgt  41938  iccelpart  41944  iccpartiun  41945  icceuelpartlem  41946  icceuelpart  41947  iccpartnel  41949  fargshiftf1  41952  reuccatpfxs1lem  42008  fmtnofac2  42056  fmtnofac1  42057  prmdvdsfmtnof1lem2  42072  perfectALTVlem2  42206  sbgoldbwt  42240  sbgoldbst  42241  sgoldbeven3prm  42246  sbgoldbm  42247  nnsum4primesodd  42259  nnsum4primesoddALTV  42260  evengpop3  42261  evengpoap3  42262  bgoldbnnsum3prm  42267  bgoldbtbndlem4  42271  bgoldbtbnd  42272  tgblthelfgott  42278  tgoldbach  42280  sprsymrelfolem2  42311  ply1mulgsumlem2  42743  islininds  42803  linindslinci  42805  lindslinindsimp1  42814  linds0  42822  lindsrng01  42825  snlindsntorlem  42827  snlindsntor  42828  ldepsnlinc  42865  nn0sumshdiglemA  42981  nn0sumshdiglemB  42982  nn0sumshdiglem1  42983  nn0sumshdiglem2  42984  nn0sumshdig  42985  bnd2d  42996  setrec1lem1  43002  setrec1lem4  43005  setrec2fun  43007