Theorem imbi12d 337

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  imbi12  339  nfbiit  1813  nfbidv  1881  sbjust  2014  nfbidf  2156  axc15OLD  2358  drnf1  2379  mobidvOLDOLD  2619  mobidOLDOLD  2626  axext3ALT  2753  ralcom2  3304  raleqbidv  3341  cbvralf  3377  cbvraldva2  3387  vtoclgaf  3492  vtoclga  3493  vtocl2gaf  3495  vtocl3gaf  3496  vtocl4ga  3499  rspct  3527  rspc  3529  rspc2gv  3547  rexraleqim  3555  ralab2  3604  nelrdva  3610  mob2  3622  mob  3624  morex  3626  reu7  3637  reu8  3638  reu2eqd  3641  cdeqim  3675  sbcimg  3726  csbhypf  3809  cbvralcsf  3822  dfss2f  3851  reusngf  4487  rexreusng  4492  reuprg0  4513  elpreqpr  4672  elintab  4761  intss1  4765  intmin  4770  dfiin2g  4828  trel  5038  zfpow  5121  reusv2lem4  5156  reusv3i  5159  rext  5198  opth  5226  copsexg  5239  poeq1  5330  pocl  5334  swopolem  5336  swopo  5337  isso2i  5361  fri  5370  vtoclr  5466  poinxp  5483  posn  5488  ssrel  5508  ssrel2  5510  ssrelrel  5520  relop  5572  reu3op  5983  reuop  5984  predbrg  6008  preddowncl  6015  wfisg  6023  ordelord  6053  iota5  6174  sbcfung  6214  funopg  6224  brprcneu  6493  tz6.12f  6525  funbrfv  6548  ssimaexg  6579  fvmptf  6617  fvelrn  6671  fprg  6742  dff13f  6841  f1veqaeq  6842  fpropnf1  6852  soisores  6905  soisoi  6906  isofrlem  6918  isopolem  6923  weniso  6932  riota5f  6964  imbrov2fvoveq  7003  oprabid  7009  f1opr  7031  ovmpos  7116  ov2gf  7117  ov3  7129  caovcan  7170  caovordig  7171  caofrss  7262  caoftrn  7264  tfis  7387  tfisi  7391  tfindsg  7393  tfindsg2  7394  tfindes  7395  dfom2  7400  limomss  7403  nnlim  7411  findsg  7426  findes  7429  f1oweALT  7487  dfoprab4f  7564  offval22  7593  f1o2ndf1  7625  frxp  7627  poxp  7629  suppfnss  7660  wfrdmcl  7769  onfununi  7784  smoel  7803  smogt  7810  tfrlem1  7818  tz7.48lem  7882  tz7.49  7886  oawordeu  7984  omordi  7995  oeordi  8016  nnmordi  8060  omabs  8076  nneob  8081  omsmolem  8082  qsel  8178  eroveu  8194  ecopovtrn  8202  ixpsnf1o  8301  fundmeng  8383  sbth  8435  limensuc  8492  nneneq  8498  php  8499  php2  8500  unxpdom  8522  pssnn  8533  findcard  8554  findcard2  8555  findcard2d  8557  findcard3  8558  ac6sfi  8559  frfi  8560  domunfican  8588  fiint  8592  iunfi  8609  finsschain  8628  dffi3  8692  marypha1lem  8694  marypha1  8695  supeq3  8710  supeq123d  8711  supmo  8713  suplub  8721  supisolem  8734  eqinf  8745  infval  8747  infmo  8756  ordiso2  8776  ordtypelem7  8785  wemaplem1  8807  wemaplem2  8808  zfregcl  8855  inf0  8880  inf3lem1  8887  zfinf  8898  axinf2  8899  dfom3  8906  elom3  8907  cantnfval2  8928  cantnfle  8930  cantnflt  8931  cantnfp1lem3  8939  oemapvali  8943  cantnflem1c  8946  cantnflem1  8948  cantnf  8952  wemapwe  8956  cnfcom  8959  setind  8972  r1sdom  8999  r1ordg  9003  rankonidlem  9053  rankunb  9075  bnd2  9118  infxpenlem  9235  infxpenc2  9244  dfac8alem  9251  dfac8clem  9254  indcardi  9263  alephordi  9296  alephinit  9317  alephfp  9330  aceq3lem  9342  dfac5lem4  9348  dfac5  9350  dfac2b  9352  dfac9  9358  dfac12lem2  9366  dfac12lem3  9367  kmlem1  9372  kmlem4  9375  kmlem10  9381  kmlem12  9383  kmlem13  9384  pwsdompw  9426  ackbij1lem16  9457  cfslb2n  9490  cfsmolem  9492  sornom  9499  fin2i  9517  infpssrlem4  9528  isfin2-2  9541  isfin3ds  9551  fin23lem17  9560  fin23lem32  9566  fin23lem34  9568  fin23lem35  9569  fin23lem39  9572  fin23lem41  9574  isf32lem2  9576  isf33lem  9588  isf34lem4  9599  isf34lem6  9602  fin1a2lem10  9631  axcc2lem  9658  axcc3  9660  axcc4dom  9663  dominf  9667  axdc2lem  9670  axdc3lem2  9673  ac6sg  9710  zorn2lem7  9724  zornn0g  9727  ttukeylem5  9735  ttukeylem6  9736  axdclem  9741  fodomg  9745  dominfac  9795  axrepndlem1  9814  axrepndlem2  9815  axunndlem1  9817  axunnd  9818  axpowndlem2  9820  axpowndlem3  9821  axpowndlem4  9822  axregndlem2  9825  axregnd  9826  axinfndlem1  9827  axinfnd  9828  axacndlem4  9832  axacndlem5  9833  axacnd  9834  zfcndpow  9838  zfcndinf  9840  fpwwe2lem5  9856  fpwwe2lem8  9859  fpwwe2lem12  9863  pwfseqlem4a  9883  pwfseqlem4  9884  pwfseqlem5  9885  pwfseq  9886  wunfi  9943  wunex2  9960  inar1  9997  rankcf  9999  tskord  10002  grudomon  10039  grur1a  10041  axgroth6  10050  axgroth3  10053  axgroth4  10054  eltskm  10065  indpi  10129  pinq  10149  nqereu  10151  prcdnq  10215  prnmax  10217  ltsopr  10254  prlem936  10269  ltsosr  10316  recexsrlem  10325  mulgt0sr  10327  map2psrpr  10332  supsrlem  10333  axrrecex  10385  axpre-lttrn  10388  axpre-mulgt0  10390  axpre-sup  10391  axsup  10518  dedekind  10605  ltordlem  10968  ltord1  10969  wloglei  10975  squeeze0  11346  infm3  11403  nnsub  11487  nnunb  11706  peano5uzti  11888  fzind  11896  eluzadd  12090  eluzsub  12091  uzind4s  12125  uzind4s2  12126  zmax  12162  zbtwnre  12163  xmulasslem  12497  xrsupsslem  12519  xrinfmsslem  12520  xrub  12524  infmremnf  12555  injresinj  12976  om2uzlti  13136  uzindi  13168  axdc4uz  13170  ssnn0fi  13171  rabssnn0fi  13172  suppssfz  13180  seqp1  13202  seqcl2  13206  seqfveq2  13210  seqshft2  13214  monoord  13218  seqsplit  13221  seqf1olem2  13228  seqf1o  13229  seqid2  13234  seqhomo  13235  seqof2  13246  expcl2lem  13259  facdiv  13465  facwordi  13467  faclbnd4lem2  13472  hashnn0n0nn  13568  hashf1lem2  13630  seqcoll  13638  fi1uzind  13669  brfi1indALT  13672  wrdind  13918  wrdindOLD  13919  wrd2ind  13920  wrd2indOLD  13921  reuccats1lemOLD  13923  swrdccatin1  13927  swrdccat3blem  13947  reuccatpfxs1lem  13958  repswccat  14008  cshf1  14037  trclfvcotr  14233  relexprelg  14261  rtrclreclem4  14284  relexpindlem  14286  ello1mpt  14742  o1co  14807  o1compt  14808  rlimcn2  14811  climcn2  14813  subcn2  14815  o1of2  14833  fsumsplitf  14961  fsum2d  14989  modfsummod  15012  fsumabs  15019  telfsumo  15020  fsumrlim  15029  fsumo1  15030  o1fsum  15031  fsumiun  15039  prodfdiv  15115  fprod2d  15198  fproddivf  15204  fprodsplitf  15205  fprodsplit1f  15207  rpnnen2lem10  15439  sqrt2irr  15465  dvdsle  15523  divalglem7  15613  divalglem8  15614  ndvdssub  15623  gcdcllem1  15711  dfgcd2  15753  algcvg  15779  algcvga  15782  algfx  15783  lcmgcdlem  15809  lcmdvds  15811  lcmf  15836  lcmfunsnlem1  15840  lcmfunsnlem2lem1  15841  lcmfunsnlem  15844  lcmfdvds  15845  lcmfun  15848  coprmgcdb  15852  coprmdvds1  15855  coprmdvds2  15857  coprmprod  15864  coprmproddvds  15866  prmind2  15888  dvdsprime  15890  nprm  15891  dvdsprm  15906  exprmfct  15907  coprm  15914  isprm6  15917  prmfac1  15922  eulerthlem2  15978  pcqmul  16049  pcqcl  16052  pc2dvds  16074  pcz  16076  prmpwdvds  16099  infpn2  16108  vdwlem12  16187  ramub2  16209  rami  16210  ramcl  16224  prmdvdsprmop  16238  prmlem0  16298  mreintcl  16727  ismred2  16735  mrissmrcd  16772  mreexexlemd  16776  iscatd2  16813  moni  16867  yoniso  17396  isprs  17401  prslem  17402  drsdirfi  17409  ispos  17418  posi  17421  isposd  17426  lubfval  17449  lublecllem  17459  glbfval  17462  joinle  17485  meetle  17499  lubl  17591  lubun  17594  clatleglb  17597  pospropd  17605  poslubmo  17617  posglbmo  17618  ipodrsima  17636  acsdrsel  17638  isacs4lem  17639  isacs5lem  17640  acsdrscl  17641  mreclatBAD  17658  pslem  17677  dirtr  17707  mndind  17837  mhmlem  18009  isnsg2  18096  ghmf1  18161  orbsta  18217  symgextf1  18313  gsmsymgrfix  18320  gsmsymgreq  18324  symggen  18362  psgnunilem4  18390  sylow1lem1  18487  sylow2alem2  18507  sylow2a  18508  lsmmod  18562  lsmdisj2  18569  efgsrel  18621  efgredlemd  18632  efgredlem  18635  efgredlemOLD  18636  efgred  18637  gsumzaddlem  18797  gsummptnn0fz  18859  gsummptnn0fzfv  18860  telgsumfzs  18862  telgsums  18866  dprdval  18878  dprddisj2  18914  ablfac1eulem  18947  pgpfac1lem1  18949  pgpfac1lem5  18954  pgpfac1  18955  pgpfaclem2  18957  pgpfac  18959  irredmul  19185  f1rhm0to0ALT  19220  isdrngrd  19254  sdrgacs  19305  islbs3  19652  rrgval  19784  rrgeq0i  19786  isdomn  19791  domneq0  19794  mplsubglem  19931  mpllsslem  19932  mplcoe1  19962  mplcoe5  19965  mpfind  20032  coe1fzgsumd  20176  gsummoncoe1  20178  pf1ind  20223  evl1gsumd  20225  prmirredlem  20345  znfld  20412  znrrg  20417  cygznlem3  20421  isphl  20477  ipeq0  20487  isphld  20503  phlpropd  20504  lsmcss  20541  frlmphl  20630  frlmup1  20647  lindfrn  20670  islindf4  20687  islindf5  20688  dmatelnd  20812  mat1scmat  20855  mdetdiaglem  20914  mdetralt  20924  mdetralt2  20925  mdetunilem1  20928  mdetunilem2  20929  mdetunilem3  20930  mdetunilem4  20931  mdetunilem9  20936  smadiadetr  20991  pmatcoe1fsupp  21016  mp2pm2mplem4  21124  uniopn  21212  fiinopn  21216  epttop  21324  clsndisj  21390  elcls3  21398  neiptoptop  21446  neiptopnei  21447  cnpval  21551  iscnp  21552  cnpimaex  21571  lmcvg  21577  cnprest  21604  cnprest2  21605  lmss  21613  lmff  21616  t0sep  21639  hausnei  21643  isnrm2  21673  t1sep2  21684  isreg2  21692  iscmp  21703  cmpcov  21704  cmpsublem  21714  cmpsub  21715  tgcmp  21716  uncmp  21718  fiuncmp  21719  hauscmplem  21721  cmpfi  21723  cmpfii  21724  dfconn2  21734  connsuba  21735  connsub  21736  nconnsubb  21738  1stcclb  21759  1stcfb  21760  2ndc1stc  21766  1stcrest  21768  1stcelcls  21776  restnlly  21797  lly1stc  21811  comppfsc  21847  kgenval  21850  kgeni  21852  kgencn2  21872  ptcldmpt  21929  ptclsg  21930  dfac14lem  21932  dfac14  21933  txcnp  21935  ptcnp  21937  hausdiag  21960  txlm  21963  tx1stc  21965  xkococn  21975  cnmpt12  21982  cnmpt22  21989  kqt0lem  22051  isr0  22052  regr1lem2  22055  kqreglem1  22056  r0sep  22063  ptcmpfi  22128  elmptrab  22142  isfil  22162  filss  22168  isufil2  22223  cfinufil  22243  rnelfm  22268  fmfnfmlem2  22270  fmfnfmlem4  22272  flimopn  22290  flimrest  22298  flftg  22311  cnpflf  22316  txflf  22321  fclsopni  22330  fclsrest  22339  fclscf  22340  flimfnfcls  22343  fcfnei  22350  alexsublem  22359  alexsubb  22361  alexsubALTlem3  22364  alexsubALTlem4  22365  alexsubALT  22366  cnextcn  22382  cnextfres1  22383  tgpt0  22433  qustgplem  22435  tsmsi  22448  tsmssubm  22457  tsmsres  22458  tsmsf1o  22459  tsmsxp  22469  ustssel  22520  ust0  22534  ustuqtop4  22559  ucnima  22596  ucncn  22600  iscusp  22614  cuspcvg  22616  imasdsf1olem  22689  blssps  22740  blss  22741  metss  22824  comet  22829  metcnp3  22856  metcnp2  22858  txmetcnp  22863  metuel2  22881  metucn  22887  nrmmetd  22890  nlmvscn  23002  nrginvrcn  23007  nmolb  23032  xrge0tsms  23148  divcn  23182  fsumcn  23184  elcncf2  23204  cncfi  23208  mulc1cncf  23219  cncfmet  23222  xrhmeo  23256  bndth  23268  nmoleub2lem2  23426  nmoleub3  23429  ipcn  23555  lmmbr  23567  caucfil  23592  pmltpc  23757  ovolfiniun  23808  ovolicc2lem3  23826  ovolicc2  23829  mblsplit  23839  finiunmbl  23851  volfiniun  23854  voliunlem3  23859  ioorinv  23883  ioorcl  23884  dyadmax  23905  dyadmbllem  23906  dyadmbl  23907  opnmbllem  23908  volcn  23913  vitalilem2  23916  vitalilem3  23917  vitali  23920  i1fd  23988  itg2seq  24049  itg2addlem  24065  itgfsum  24133  ellimc3  24183  dvbsss  24206  dvnres  24234  dvmptfsum  24278  dvferm1lem  24287  dvferm2lem  24289  rolle  24293  c1lip1  24300  lhop1lem  24316  lhop1  24317  dvfsumlem2  24330  dvfsumlem4  24332  dvfsumrlim  24334  dvfsum2  24337  ftc1a  24340  ftc1lem6  24344  mdegleb  24364  mdeglt  24365  deg1leb  24395  deg1lt  24397  ply1divex  24436  fta1glem2  24466  fta1g  24467  plyco0  24488  plyeq0lem  24506  coeeq2  24538  dgrle  24539  dgrcolem2  24570  dgrco  24571  plydivlem4  24591  plydivex  24592  fta1lem  24602  fta1  24603  vieta1lem2  24606  vieta1  24607  aalioulem2  24628  aalioulem4  24630  abelth  24735  cxpcn3  25033  rlimcnp  25248  xrlimcnp  25251  cxploglim  25260  scvxcvx  25268  jensen  25271  lgamgulmlem2  25312  wilthlem2  25351  wilthlem3  25352  fta  25362  dvdsmulf1o  25476  perfectlem2  25511  dchrelbas3  25519  dchrelbas4  25524  dchrn0  25531  bcmono  25558  lgsdir2lem4  25609  lgsdchr  25636  gausslemma2dlem0i  25645  lgseisenlem2  25657  lgsquad2lem2  25666  2sqlem6  25704  2sqlem8  25707  2sqlem10  25709  dchrisumlema  25769  dchrisumlem2  25771  dchrisumlem3  25772  istrkgb  25946  istrkgcb  25947  istrkge  25948  axtgcgrid  25954  axtg5seg  25956  axtgbtwnid  25957  axtgpasch  25958  axtgcont1  25959  axtgeucl  25963  iscgrglt  26005  tgcgr4  26022  axcgrtr  26407  gropd  26522  grstructd  26523  upgredg2vtx  26632  upgredgpr  26633  edglnl  26634  numedglnl  26635  usgredg2vtxeuALT  26710  nbgr2vtx1edg  26838  finsumvtxdg2size  27038  wlkp1lem8  27171  upgrwlkdvdelem  27228  usgr2wlkneq  27248  usgr2pthlem  27255  pthdlem2lem  27259  uspgrn2crct  27297  2pthdlem1  27439  eleclclwwlkn  27603  hashecclwwlkn1  27604  umgrhashecclwwlk  27605  3pthdlem1  27696  eupth2  27772  frgr3vlem1  27810  3vfriswmgrlem  27814  frgrwopreglem4a  27847  frgr2wwlk1  27866  wlkl0  27923  numclwlk2lem2f1o  27935  numclwlk2lem2f1oOLD  27938  friendshipgt3  27958  eulplig  28042  nvz  28226  nmobndseqi  28336  nmobndseqiALT  28337  nmlno0  28352  blocnilem  28361  dipdir  28399  dipass  28402  siilem2  28409  ubthlem2  28429  ubth  28431  htth  28477  normpyth  28704  norm3lemt  28711  chlimi  28793  chcompl  28801  omlsii  28964  pjoml  28997  h1de2i  29114  elspansn2  29128  h1datom  29143  pjoml2  29172  pjoml3  29173  lecm  29178  chscllem2  29199  osum  29206  spansncv  29214  pjcjt2  29253  pjopyth  29281  eigre  29396  eigorth  29399  hhcno  29465  hhcnf  29466  cnopc  29474  cnfnc  29491  nmcexi  29587  nmcopexi  29588  nmcfnexi  29612  pjssge0i  29727  hstel2  29780  stj  29796  stri  29818  hstri  29826  stcltr1i  29835  mdbr  29855  mdi  29856  mdbr3  29858  mdbr4  29859  dmdbr  29860  dmdmd  29861  dmdi  29863  dmdbr3  29866  dmdbr4  29867  dmdbr5  29869  mdsl1i  29882  mdslmd1lem3  29888  mdslmd1lem4  29889  mdslmd1i  29890  csmdsymi  29895  cvmd  29897  atss  29907  atom1d  29914  chcv1  29916  hatomic  29921  atord  29949  atcvat2  29950  mddmdin0i  29992  opreu2reuALT  30025  rmoxfrd  30041  ifeqeqx  30068  ssiun2sf  30083  ssrelf  30133  fmptcof2  30167  acunirnmpt  30169  acunirnmpt2  30170  acunirnmpt2f  30171  aciunf1lem  30172  suppovss  30190  fz1nntr  30277  nn0min  30286  fsumiunle  30294  ressprs  30374  resspos  30378  toslublem  30386  tosglblem  30388  isomnd  30420  omndadd  30425  submarchi  30481  archirng  30483  archiexdiv  30485  archiabllem1a  30486  archiabllem2a  30489  archiabl  30493  gsumle  30522  gsumvsca1  30525  gsumvsca2  30526  xrge0tsmsd  30530  isorng  30551  orngmul  30555  isarchiofld  30569  linds2eq  30612  lbsdiflsp0  30651  fedgmullem1  30654  fedgmullem2  30655  fzto1st  30694  psgnfzto1st  30696  submateq  30716  lmatfval  30721  lmatcl  30723  iscref  30752  crefi  30755  pcmplfin  30768  xrge0iifiso  30822  esumcvg  30989  esum2dlem  30995  isrnsigaOLD  31016  sigaclcu  31021  sigaclci  31036  unelsiga  31038  unelldsys  31062  sigapildsys  31066  ldgenpisyslem1  31067  fiunelros  31078  measvun  31113  measiun  31122  carsgmon  31217  carsgsigalem  31218  carsgclctunlem2  31222  carsgclctun  31224  pmeasmono  31227  pmeasadd  31228  sibfof  31243  sitgclg  31245  eulerpartlemgvv  31279  signsply0  31467  signstfvneq0  31489  breprexp  31552  hgt749d  31568  istrkg2d  31585  axtgupdim2OLD  31587  bnj1385  31752  bnj110  31777  bnj222  31802  bnj229  31803  bnj590  31829  bnj865  31842  bnj849  31844  bnj981  31869  bnj1014  31879  bnj1015  31880  bnj1112  31900  bnj1118  31901  bnj1123  31903  bnj1128  31907  bnj1125  31909  bnj1148  31913  bnj1154  31916  bnj1326  31943  bnj1384  31949  bnj1489  31973  bnj1497  31977  subfacp1lem6  32017  erdszelem9  32031  kur14lem9  32046  sconnpht  32061  cvmsss2  32106  cvmliftlem7  32123  cvmliftlem10  32126  fmlasuc  32196  mclsrcl  32328  mclsssvlem  32329  mclsval  32330  mclsax  32336  mclsind  32337  mclsppslem  32350  iota5f  32475  dfpo2  32511  fununiq  32532  setinds  32543  dfon2lem3  32550  dfon2lem4  32551  dfon2lem5  32552  dfon2lem6  32553  dfon2lem7  32554  dfon2lem8  32555  dfon2  32557  tfisg  32576  frpoinsg  32602  frmin  32605  frinsg  32608  noprefixmo  32723  nosupdm  32725  nosupfv  32727  nosupres  32728  nosupbnd1lem1  32729  nosupbnd1lem3  32731  nosupbnd1lem5  32733  nosupbnd2  32737  nocvxminlem  32768  btwnconn1lem11  33079  linethru  33135  fwddifnp1  33147  rankelg  33150  rankeq1o  33153  subtr  33183  subtr2  33184  trer  33185  nn0prpwlem  33191  nn0prpw  33192  neibastop2lem  33229  filnetlem4  33250  bj-hbxfrbi  33474  bj-ssblem1  33495  bj-ssblem2  33496  bj-ax12  33498  bj-drnf1v  33595  bj-axext3  33602  relowlssretop  34086  rdgeqoa  34093  rdgssun  34101  exrecfnlem  34102  finxpreclem6  34118  pibp19  34136  pibt2  34139  wl-mo3t  34253  wl-sb8mot  34255  finixpnum  34318  matunitlindflem1  34329  ptrest  34332  poimirlem13  34346  poimirlem14  34347  poimirlem17  34350  poimirlem18  34351  poimirlem20  34353  poimirlem21  34354  poimirlem22  34355  poimirlem24  34357  poimirlem25  34358  poimirlem26  34359  poimirlem28  34361  poimirlem30  34363  poimirlem31  34364  poimirlem32  34365  poimir  34366  heicant  34368  mblfinlem1  34370  mblfinlem2  34371  mblfinlem3  34372  voliunnfl  34377  volsupnfl  34378  mbfresfi  34379  itg2addnclem3  34386  ftc1cnnc  34407  ftc1anclem7  34414  ftc1anc  34416  sdclem2  34459  fdc  34462  fdc1  34463  neificl  34470  mettrifi  34474  sstotbnd2  34494  cntotbnd  34516  heibor1lem  34529  bfp  34544  isass  34566  ismgmOLD  34570  isexid2  34575  iscringd  34718  ispridl  34754  pridl  34757  ismaxidl  34760  maxidlmax  34763  ispridlc  34790  pridlc  34791  dmnnzd  34795  relcnveq2  35024  ecin0  35052  elrelscnveq2  35178  elsymrels3  35235  eltrrels3  35261  eleqvrels3  35273  eqvrelqsel  35296  axc11n-16  35519  ax12eq  35522  ax12el  35523  ax12inda  35529  ax12v2-o  35530  fsumshftd  35533  riotasv2d  35538  lshpdisj  35568  lsmsatcv  35591  lsat0cv  35614  lcvexchlem4  35618  lcvexchlem5  35619  l1cvpat  35635  isopos  35761  oposlem  35763  isoml  35819  omllaw  35824  isatl  35880  atlex  35897  iscvlat  35904  cvlexch1  35909  glbconN  35958  hlsuprexch  35962  ps-1  36058  3atlem5  36068  psubspi  36328  llnexchb2  36450  elpcliN  36474  pclfinclN  36531  ldilval  36694  ltrnfset  36698  ltrnset  36699  ltrnu  36702  trlfset  36741  trlset  36742  trlval2  36744  cdleme25cv  36939  cdleme31so  36960  cdleme31fv  36971  cdlemefrs29bpre0  36977  cdleme32fva  37018  cdleme40v  37050  trlord  37150  cdlemkid3N  37514  cdlemkid4  37515  dihffval  37811  dihfval  37812  dihval  37813  lpolconN  38068  mapdordlem2  38218  hdmapfval  38408  hdmapval  38409  hdmapval2  38413  nnn1suc  38594  ismrcd1  38690  ismrcd2  38691  ismrc  38693  isnacs3  38702  nacsfix  38704  mzpcompact2  38744  fphpd  38809  fphpdo  38810  monotuz  38934  monotoddzzfi  38935  monotoddzz  38936  oddcomabszz  38937  zindbi  38939  setindtrs  39018  dford3lem2  39020  ttac  39029  dnnumch1  39040  fnwe2lem2  39047  aomclem3  39052  aomclem6  39055  aomclem8  39057  dfac11  39058  dfac21  39062  islssfg2  39067  hbtlem5  39124  hbt  39126  flcidc  39170  mendlmod  39189  ifpbi123  39252  rababg  39295  elmapintrab  39298  iunrelexpuztr  39427  frege92  39664  frege104  39676  ntrkbimka  39751  ntrk0kbimka  39752  neik0pk1imk0  39760  isotone1  39761  isotone2  39762  ntrclsiso  39780  ntrclskb  39782  ntrneiiso  39804  ntrneik3  39809  ntrneix3  39810  gneispacess2  39859  grur1cld  39943  scottabf  39951  ismnu  39972  mnuop23d  39977  mnuunid  39988  dvgrat  40060  cvgdvgrat  40061  binomcxplemnotnn0  40104  pm14.122b  40172  sbiota1  40183  fnchoice  40705  fiiuncl  40747  iunincfi  40782  disjf1  40868  wessf1ornlem  40870  disjinfi  40879  axccdom  40913  dmrelrnrel  40916  axccd  40922  monoords  40994  fperiodmullem  41000  supxrgere  41031  supxrgelem  41035  supxrge  41036  xrlexaddrp  41050  infxr  41065  infleinf  41070  supxrleubrnmptf  41159  monoordxrv  41190  monoordxr  41191  monoord2xr  41193  fsumclf  41282  fsummulc1f  41283  fsumnncl  41284  fsumsplit1  41285  fsumf1of  41287  fsumreclf  41289  fsumlessf  41290  fsumsermpt  41292  fmul01  41293  fmulcl  41294  fmuldfeqlem1  41295  fmuldfeq  41296  fmul01lt1lem1  41297  fmul01lt1lem2  41298  fprodexp  41307  fprodabs2  41308  fprodcnlem  41312  climmulf  41317  climexp  41318  climsuse  41321  climrecf  41322  climinff  41324  climaddf  41328  mullimc  41329  mullimcf  41336  limcperiod  41341  sumnnodd  41343  lptre2pt  41353  limsupre  41354  neglimc  41360  addlimc  41361  0ellimcdiv  41362  limclner  41364  climsubmpt  41373  climreclf  41377  climeldmeqmpt  41381  climfveqmpt  41384  fnlimfvre  41387  climfveqf  41393  climfveqmpt3  41395  climeldmeqf  41396  limsupref  41398  limsupbnd1f  41399  climeqf  41401  climeldmeqmpt3  41402  climinf2  41420  limsupubuz  41426  climinf2mpt  41427  climinfmpt  41428  limsupmnf  41434  limsupequz  41436  limsupre2  41438  limsupequzmptf  41444  limsupre3  41446  lmbr3  41460  cnrefiisp  41543  xlimxrre  41544  xlimmnfvlem1  41545  xlimpnfvlem1  41549  climxlim2lem  41558  cncfshift  41588  cncfperiod  41593  icccncfext  41601  fprodcncf  41615  fperdvper  41634  dvmptmulf  41653  dvnmptdivc  41654  dvnmul  41659  dvmptfprod  41661  dvnprodlem1  41662  dvnprodlem2  41663  dvnprodlem3  41664  iblspltprt  41689  itgspltprt  41695  stoweidlem3  41720  stoweidlem4  41721  stoweidlem6  41723  stoweidlem8  41725  stoweidlem15  41732  stoweidlem16  41733  stoweidlem17  41734  stoweidlem19  41736  stoweidlem20  41737  stoweidlem22  41739  stoweidlem23  41740  stoweidlem26  41743  stoweidlem27  41744  stoweidlem30  41747  stoweidlem31  41748  stoweidlem32  41749  stoweidlem34  41751  stoweidlem35  41752  stoweidlem42  41759  stoweidlem43  41760  stoweidlem48  41765  stoweidlem50  41767  stoweidlem51  41768  stoweidlem57  41774  stoweidlem59  41776  stoweidlem62  41779  wallispilem3  41784  dirkercncflem2  41821  fourierdlem11  41835  fourierdlem12  41836  fourierdlem15  41839  fourierdlem16  41840  fourierdlem21  41845  fourierdlem34  41858  fourierdlem41  41865  fourierdlem42  41866  fourierdlem46  41869  fourierdlem48  41871  fourierdlem49  41872  fourierdlem50  41873  fourierdlem51  41874  fourierdlem68  41891  fourierdlem71  41894  fourierdlem72  41895  fourierdlem73  41896  fourierdlem76  41899  fourierdlem79  41902  fourierdlem81  41904  fourierdlem83  41906  fourierdlem86  41909  fourierdlem89  41912  fourierdlem90  41913  fourierdlem91  41914  fourierdlem92  41915  fourierdlem94  41917  fourierdlem97  41920  fourierdlem103  41926  fourierdlem104  41927  fourierdlem111  41934  fourierdlem112  41935  fourierdlem113  41936  etransclem2  41953  etransclem46  41997  salunicl  42033  saluncl  42034  intsaluni  42044  dfsalgen2  42056  sge0f1o  42096  sge0lempt  42124  sge0iunmptlemfi  42127  sge0p1  42128  sge0fodjrnlem  42130  sge0iunmpt  42132  sge0ltfirpmpt2  42140  sge0isummpt2  42146  sge0xaddlem2  42148  sge0xadd  42149  nnfoctbdjlem  42169  meadjuni  42171  meadjiun  42180  voliunsge0lem  42186  meaiuninclem  42194  meaiunincf  42197  meaiuninc3v  42198  meaiuninc3  42199  meaiininclem  42200  meaiininc  42201  omeunile  42219  isomenndlem  42244  ovn0lem  42279  ovnsubaddlem1  42284  hoidmvlelem2  42310  hoidmvlelem3  42311  hoidmvlelem4  42312  hoidmvle  42314  hspmbllem2  42341  hoimbl2  42379  vonhoire  42386  vonicclem2  42398  vonn0ioo2  42404  vonn0icc2  42406  salpreimagelt  42418  salpreimalegt  42420  pimdecfgtioc  42425  pimincfltioc  42426  pimincfltioo  42428  salpreimagtge  42434  salpreimaltle  42435  salpreimagtlt  42439  incsmf  42451  decsmf  42475  smflimlem1  42479  smflimlem2  42480  smflimlem3  42481  smflimlem4  42482  smfpimcclem  42513  funressnmo  42688  aiota0def  42701  euoreqb  42715  2reu8i  42719  2reuimp0  42720  funressndmafv2rn  42829  funressnbrafv2  42850  funbrafv2  42853  smonoord  42938  iccpartgt  42960  iccelpart  42966  iccpartiun  42967  icceuelpartlem  42968  icceuelpart  42969  iccpartnel  42971  fargshiftf1  42974  ichexmpl2  43001  ichnreuop  43003  ichreuopeq  43004  sprsymrelfolem2  43024  prproropf1olem4  43037  paireqne  43042  reupr  43053  reuopreuprim  43057  fmtnofac2  43100  fmtnofac1  43101  prmdvdsfmtnof1lem2  43116  perfectALTVlem2  43256  nfermltl8rev  43276  nfermltl2rev  43277  sbgoldbwt  43311  sbgoldbst  43312  sgoldbeven3prm  43317  sbgoldbm  43318  nnsum4primesodd  43330  nnsum4primesoddALTV  43331  evengpop3  43332  evengpoap3  43333  bgoldbnnsum3prm  43338  bgoldbtbndlem4  43342  bgoldbtbnd  43343  tgblthelfgott  43349  tgoldbach  43351  isomuspgrlem2b  43363  ply1mulgsumlem2  43809  islininds  43869  linindslinci  43871  lindslinindsimp1  43880  linds0  43888  lindsrng01  43891  snlindsntorlem  43893  snlindsntor  43894  ldepsnlinc  43931  nn0sumshdiglemA  44048  nn0sumshdiglemB  44049  nn0sumshdiglem1  44050  nn0sumshdiglem2  44051  nn0sumshdig  44052  itschlc0yqe  44116  bnd2d  44152  setrec1lem1  44158  setrec1lem4  44161  setrec2fun  44163