Theorem imbi12d 347

Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993.)

Hypotheses

Ref	Expression
imbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
imbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
imbi12d	⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	imbi1d 344	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 343	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	bitrd 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  349  ifpbi123d  1072  nfbiit  1851  nfbidv  1923  sbjust  2068  nfbidf  2226  drnf1v  2389  drnf1  2465  mo4  2650  axextg  2795  ralcom2  3363  raleqbidv  3401  cbvralfw  3437  cbvralf  3439  cbvralvw  3449  cbvraldva2  3456  vtoclgaf  3573  vtoclga  3574  vtocl2gaf  3576  vtocl3gaf  3577  vtocl4ga  3580  rspct  3609  rspc  3611  rspc2gv  3632  rexraleqim  3640  ralab2  3688  ralab2OLD  3689  nelrdva  3696  mob2  3706  mob  3708  morex  3710  reu7  3723  reu8  3724  reu2eqd  3727  cdeqim  3764  sbcimg  3820  csbhypf  3911  cbvralcsf  3925  dfss2f  3958  reusngf  4612  rexreusng  4617  reuprg0  4638  elpreqpr  4797  elintab  4887  intss1  4891  intmin  4896  dfiin2g  4957  trel  5179  zfpow  5267  reusv2lem4  5302  reusv3i  5305  rext  5341  opth  5368  copsexgw  5381  copsexg  5382  poeq1  5477  pocl  5481  swopolem  5483  swopo  5484  isso2i  5508  fri  5517  vtoclr  5615  poinxp  5632  posn  5637  ssrel  5657  ssrel2  5659  ssrelrel  5669  relop  5721  reu3op  6143  reuop  6144  predbrg  6168  preddowncl  6175  wfisg  6183  ordelord  6213  iota5  6338  sbcfung  6379  funopg  6389  brprcneu  6662  tz6.12f  6694  funbrfv  6716  ssimaexg  6749  fvmptf  6789  fvelrn  6844  fprg  6917  dff13f  7014  f1veqaeq  7015  fpropnf1  7025  nf1const  7059  soisores  7080  soisoi  7081  isofrlem  7093  isopolem  7098  weniso  7107  riota5f  7142  imbrov2fvoveq  7181  oprabidw  7187  oprabid  7188  f1opr  7210  ovmpos  7298  ov2gf  7299  ov3  7311  caovcan  7352  caovordig  7353  caofrss  7442  caoftrn  7444  tfis  7569  tfisi  7573  tfindsg  7575  tfindsg2  7576  tfindes  7577  dfom2  7582  limomss  7585  nnlim  7593  findsg  7609  findes  7612  f1oweALT  7673  dfoprab4f  7754  offval22  7783  f1o2ndf1  7818  frxp  7820  poxp  7822  suppfnss  7855  wfrdmcl  7963  onfununi  7978  smoel  7997  smogt  8004  tfrlem1  8012  tz7.48lem  8077  tz7.49  8081  oawordeu  8181  omordi  8192  oeordi  8213  nnmordi  8257  omabs  8274  nneob  8279  omsmolem  8280  qsel  8376  eroveu  8392  ecopovtrn  8400  ixpsnf1o  8502  fundmeng  8584  sbth  8637  limensuc  8694  nneneq  8700  php  8701  php2  8702  unxpdom  8725  pssnn  8736  findcard  8757  findcard2  8758  findcard2d  8760  findcard3  8761  ac6sfi  8762  frfi  8763  domunfican  8791  fiint  8795  iunfi  8812  finsschain  8831  dffi3  8895  marypha1lem  8897  marypha1  8898  supeq3  8913  supeq123d  8914  supmo  8916  suplub  8924  supisolem  8937  eqinf  8948  infval  8950  infmo  8959  ordiso2  8979  ordtypelem7  8988  wemaplem1  9010  wemaplem2  9011  zfregcl  9058  inf0  9084  inf3lem1  9091  zfinf  9102  axinf2  9103  dfom3  9110  elom3  9111  cantnfval2  9132  cantnfle  9134  cantnflt  9135  cantnfp1lem3  9143  oemapvali  9147  cantnflem1c  9150  cantnflem1  9152  cantnf  9156  wemapwe  9160  cnfcom  9163  setind  9176  r1sdom  9203  r1ordg  9207  rankonidlem  9257  rankunb  9279  bnd2  9322  infxpenlem  9439  infxpenc2  9448  dfac8alem  9455  dfac8clem  9458  indcardi  9467  alephordi  9500  alephinit  9521  alephfp  9534  aceq3lem  9546  dfac5lem4  9552  dfac5  9554  dfac2b  9556  dfac9  9562  dfac12lem2  9570  dfac12lem3  9571  kmlem1  9576  kmlem4  9579  kmlem10  9585  kmlem12  9587  kmlem13  9588  pwsdompw  9626  ackbij1lem16  9657  cfslb2n  9690  cfsmolem  9692  sornom  9699  fin2i  9717  infpssrlem4  9728  isfin2-2  9741  isfin3ds  9751  fin23lem17  9760  fin23lem32  9766  fin23lem34  9768  fin23lem35  9769  fin23lem39  9772  fin23lem41  9774  isf32lem2  9776  isf33lem  9788  isf34lem4  9799  isf34lem6  9802  fin1a2lem10  9831  axcc2lem  9858  axcc3  9860  axcc4dom  9863  dominf  9867  axdc2lem  9870  axdc3lem2  9873  ac6sg  9910  zorn2lem7  9924  zornn0g  9927  ttukeylem5  9935  ttukeylem6  9936  axdclem  9941  fodomg  9945  dominfac  9995  axrepndlem1  10014  axrepndlem2  10015  axunndlem1  10017  axunnd  10018  axpowndlem2  10020  axpowndlem3  10021  axpowndlem4  10022  axregndlem2  10025  axregnd  10026  axinfndlem1  10027  axinfnd  10028  axacndlem4  10032  axacndlem5  10033  axacnd  10034  zfcndpow  10038  zfcndinf  10040  fpwwe2lem5  10056  fpwwe2lem8  10059  fpwwe2lem12  10063  pwfseqlem4a  10083  pwfseqlem4  10084  pwfseqlem5  10085  pwfseq  10086  wunfi  10143  wunex2  10160  inar1  10197  rankcf  10199  tskord  10202  grudomon  10239  grur1a  10241  axgroth6  10250  axgroth3  10253  axgroth4  10254  eltskm  10265  indpi  10329  pinq  10349  nqereu  10351  prcdnq  10415  prnmax  10417  ltsopr  10454  prlem936  10469  ltsosr  10516  recexsrlem  10525  mulgt0sr  10527  map2psrpr  10532  supsrlem  10533  axrrecex  10585  axpre-lttrn  10588  axpre-mulgt0  10590  axpre-sup  10591  axsup  10716  dedekind  10803  ltordlem  11165  ltord1  11166  wloglei  11172  squeeze0  11543  infm3  11600  nnsub  11682  nnunb  11894  peano5uzti  12073  fzind  12081  eluzadd  12274  eluzsub  12275  uzind4s  12309  uzind4s2  12310  zmax  12346  zbtwnre  12347  xmulasslem  12679  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  infmremnf  12737  injresinj  13159  om2uzlti  13319  uzindi  13351  axdc4uz  13353  ssnn0fi  13354  rabssnn0fi  13355  suppssfz  13363  seqp1  13385  seqcl2  13389  seqfveq2  13393  seqshft2  13397  monoord  13401  seqsplit  13404  seqf1olem2  13411  seqf1o  13412  seqid2  13417  seqhomo  13418  seqof2  13429  expcl2lem  13442  facdiv  13648  facwordi  13650  faclbnd4lem2  13655  hashnn0n0nn  13753  hashf1lem2  13815  seqcoll  13823  fi1uzind  13856  brfi1indALT  13859  wrdind  14084  wrd2ind  14085  swrdccatin1  14087  swrdccat3blem  14101  reuccatpfxs1lem  14108  repswccat  14148  cshf1  14172  trclfvcotr  14369  relexprelg  14397  rtrclreclem4  14420  relexpindlem  14422  ello1mpt  14878  o1co  14943  o1compt  14944  rlimcn2  14947  climcn2  14949  subcn2  14951  o1of2  14969  fsumsplitf  15098  fsum2d  15126  modfsummod  15149  fsumabs  15156  telfsumo  15157  fsumrlim  15166  fsumo1  15167  o1fsum  15168  fsumiun  15176  prodfdiv  15252  fprod2d  15335  fproddivf  15341  fprodsplitf  15342  fprodsplit1f  15344  rpnnen2lem10  15576  sqrt2irr  15602  dvdsle  15660  divalglem7  15750  divalglem8  15751  ndvdssub  15760  gcdcllem1  15848  dfgcd2  15894  algcvg  15920  algcvga  15923  algfx  15924  lcmgcdlem  15950  lcmdvds  15952  lcmf  15977  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem  15985  lcmfdvds  15986  lcmfun  15989  coprmgcdb  15993  coprmdvds1  15996  coprmdvds2  15998  coprmprod  16005  coprmproddvds  16007  prmind2  16029  dvdsprime  16031  nprm  16032  dvdsprm  16047  exprmfct  16048  coprm  16055  isprm6  16058  prmfac1  16063  eulerthlem2  16119  pcqmul  16190  pcqcl  16193  pc2dvds  16215  pcz  16217  prmpwdvds  16240  infpn2  16249  vdwlem12  16328  ramub2  16350  rami  16351  ramcl  16365  prmdvdsprmop  16379  prmlem0  16439  mreintcl  16866  ismred2  16874  mrissmrcd  16911  mreexexlemd  16915  iscatd2  16952  moni  17006  yoniso  17535  isprs  17540  prslem  17541  drsdirfi  17548  ispos  17557  posi  17560  isposd  17565  lubfval  17588  lublecllem  17598  glbfval  17601  joinle  17624  meetle  17638  lubl  17730  lubun  17733  clatleglb  17736  pospropd  17744  poslubmo  17756  posglbmo  17757  ipodrsima  17775  acsdrsel  17777  isacs4lem  17778  isacs5lem  17779  acsdrscl  17780  mreclatBAD  17797  pslem  17816  dirtr  17846  mndind  17992  mhmlem  18219  isnsg2  18308  ghmf1  18387  orbsta  18443  symgextf1  18549  gsmsymgrfix  18556  gsmsymgreq  18560  symggen  18598  psgnunilem4  18625  sylow1lem1  18723  sylow2alem2  18743  sylow2a  18744  lsmmod  18801  lsmdisj2  18808  efgsrel  18860  efgredlemd  18870  efgredlem  18873  efgred  18874  gsumzaddlem  19041  gsummptnn0fz  19106  gsummptnn0fzfv  19107  telgsumfzs  19109  telgsums  19113  dprdval  19125  dprddisj2  19161  ablfac1eulem  19194  pgpfac1lem1  19196  pgpfac1lem5  19201  pgpfac1  19202  pgpfaclem2  19204  pgpfac  19206  irredmul  19459  f1rhm0to0ALT  19494  isdrngrd  19528  sdrgacs  19580  islbs3  19927  rrgval  20060  rrgeq0i  20062  isdomn  20067  domneq0  20070  mplsubglem  20214  mpllsslem  20215  mplcoe1  20246  mplcoe5  20249  mpfind  20320  coe1fzgsumd  20470  gsummoncoe1  20472  pf1ind  20518  evl1gsumd  20520  prmirredlem  20640  znfld  20707  znrrg  20712  cygznlem3  20716  isphl  20772  ipeq0  20782  isphld  20798  phlpropd  20799  lsmcss  20836  frlmphl  20925  frlmup1  20942  lindfrn  20965  islindf4  20982  islindf5  20983  dmatelnd  21105  mat1scmat  21148  mdetdiaglem  21207  mdetralt  21217  mdetralt2  21218  mdetunilem1  21221  mdetunilem2  21222  mdetunilem3  21223  mdetunilem4  21224  mdetunilem9  21229  smadiadetr  21284  pmatcoe1fsupp  21309  mp2pm2mplem4  21417  uniopn  21505  fiinopn  21509  epttop  21617  clsndisj  21683  elcls3  21691  neiptoptop  21739  neiptopnei  21740  cnpval  21844  iscnp  21845  cnpimaex  21864  lmcvg  21870  cnprest  21897  cnprest2  21898  lmss  21906  lmff  21909  t0sep  21932  hausnei  21936  isnrm2  21966  t1sep2  21977  isreg2  21985  iscmp  21996  cmpcov  21997  cmpsublem  22007  cmpsub  22008  tgcmp  22009  uncmp  22011  fiuncmp  22012  hauscmplem  22014  cmpfi  22016  cmpfii  22017  dfconn2  22027  connsuba  22028  connsub  22029  nconnsubb  22031  1stcclb  22052  1stcfb  22053  2ndc1stc  22059  1stcrest  22061  1stcelcls  22069  restnlly  22090  lly1stc  22104  comppfsc  22140  kgenval  22143  kgeni  22145  kgencn2  22165  ptcldmpt  22222  ptclsg  22223  dfac14lem  22225  dfac14  22226  txcnp  22228  ptcnp  22230  hausdiag  22253  txlm  22256  tx1stc  22258  xkococn  22268  cnmpt12  22275  cnmpt22  22282  kqt0lem  22344  isr0  22345  regr1lem2  22348  kqreglem1  22349  r0sep  22356  ptcmpfi  22421  elmptrab  22435  isfil  22455  filss  22461  isufil2  22516  cfinufil  22536  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  flimopn  22583  flimrest  22591  flftg  22604  cnpflf  22609  txflf  22614  fclsopni  22623  fclsrest  22632  fclscf  22633  flimfnfcls  22636  fcfnei  22643  alexsublem  22652  alexsubb  22654  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  cnextcn  22675  cnextfres1  22676  tgpt0  22727  qustgplem  22729  tsmsi  22742  tsmssubm  22751  tsmsres  22752  tsmsf1o  22753  tsmsxp  22763  ustssel  22814  ust0  22828  ustuqtop4  22853  ucnima  22890  ucncn  22894  iscusp  22908  cuspcvg  22910  imasdsf1olem  22983  blssps  23034  blss  23035  metss  23118  comet  23123  metcnp3  23150  metcnp2  23152  txmetcnp  23157  metuel2  23175  metucn  23181  nrmmetd  23184  nlmvscn  23296  nrginvrcn  23301  nmolb  23326  xrge0tsms  23442  divcn  23476  fsumcn  23478  elcncf2  23498  cncfi  23502  mulc1cncf  23513  cncfmet  23516  xrhmeo  23550  bndth  23562  nmoleub2lem2  23720  nmoleub3  23723  ipcn  23849  lmmbr  23861  caucfil  23886  pmltpc  24051  ovolfiniun  24102  ovolicc2lem3  24120  ovolicc2  24123  mblsplit  24133  finiunmbl  24145  volfiniun  24148  voliunlem3  24153  ioorinv  24177  ioorcl  24178  dyadmax  24199  dyadmbllem  24200  dyadmbl  24201  opnmbllem  24202  volcn  24207  vitalilem2  24210  vitalilem3  24211  vitali  24214  i1fd  24282  itg2seq  24343  itg2addlem  24359  itgfsum  24427  ellimc3  24477  dvbsss  24500  dvnres  24528  dvmptfsum  24572  dvferm1lem  24581  dvferm2lem  24583  rolle  24587  c1lip1  24594  lhop1lem  24610  lhop1  24611  dvfsumlem2  24624  dvfsumlem4  24626  dvfsumrlim  24628  dvfsum2  24631  ftc1a  24634  ftc1lem6  24638  mdegleb  24658  mdeglt  24659  deg1leb  24689  deg1lt  24691  ply1divex  24730  fta1glem2  24760  fta1g  24761  plyco0  24782  plyeq0lem  24800  coeeq2  24832  dgrle  24833  dgrcolem2  24864  dgrco  24865  plydivlem4  24885  plydivex  24886  fta1lem  24896  fta1  24897  vieta1lem2  24900  vieta1  24901  aalioulem2  24922  aalioulem4  24924  abelth  25029  cxpcn3  25329  rlimcnp  25543  xrlimcnp  25546  cxploglim  25555  scvxcvx  25563  jensen  25566  lgamgulmlem2  25607  wilthlem2  25646  wilthlem3  25647  fta  25657  dvdsmulf1o  25771  perfectlem2  25806  dchrelbas3  25814  dchrelbas4  25819  dchrn0  25826  bcmono  25853  lgsdir2lem4  25904  lgsdchr  25931  gausslemma2dlem0i  25940  lgseisenlem2  25952  lgsquad2lem2  25961  2sqlem6  25999  2sqlem8  26002  2sqlem10  26004  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  istrkgb  26241  istrkgcb  26242  istrkge  26243  axtgcgrid  26249  axtg5seg  26251  axtgbtwnid  26252  axtgpasch  26253  axtgcont1  26254  axtgeucl  26258  iscgrglt  26300  tgcgr4  26317  axcgrtr  26701  gropd  26816  grstructd  26817  upgredg2vtx  26926  upgredgpr  26927  edglnl  26928  numedglnl  26929  usgredg2vtxeuALT  27004  nbgr2vtx1edg  27132  finsumvtxdg2size  27332  wlkp1lem8  27462  upgrwlkdvdelem  27517  usgr2wlkneq  27537  usgr2pthlem  27544  pthdlem2lem  27548  uspgrn2crct  27586  2pthdlem1  27709  eleclclwwlkn  27855  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  3pthdlem1  27943  eupth2  28018  frgr3vlem1  28052  3vfriswmgrlem  28056  frgrwopreglem4a  28089  frgr2wwlk1  28108  wlkl0  28146  numclwlk2lem2f1o  28158  friendshipgt3  28177  eulplig  28262  nvz  28446  nmobndseqi  28556  nmobndseqiALT  28557  nmlno0  28572  blocnilem  28581  dipdir  28619  dipass  28622  siilem2  28629  ubthlem2  28648  ubth  28650  htth  28695  normpyth  28922  norm3lemt  28929  chlimi  29011  chcompl  29019  omlsii  29180  pjoml  29213  h1de2i  29330  elspansn2  29344  h1datom  29359  pjoml2  29388  pjoml3  29389  lecm  29394  chscllem2  29415  osum  29422  spansncv  29430  pjcjt2  29469  pjopyth  29497  eigre  29612  eigorth  29615  hhcno  29681  hhcnf  29682  cnopc  29690  cnfnc  29707  nmcexi  29803  nmcopexi  29804  nmcfnexi  29828  pjssge0i  29943  hstel2  29996  stj  30012  stri  30034  hstri  30042  stcltr1i  30051  mdbr  30071  mdi  30072  mdbr3  30074  mdbr4  30075  dmdbr  30076  dmdmd  30077  dmdi  30079  dmdbr3  30082  dmdbr4  30083  dmdbr5  30085  mdsl1i  30098  mdslmd1lem3  30104  mdslmd1lem4  30105  mdslmd1i  30106  csmdsymi  30111  cvmd  30113  atss  30123  atom1d  30130  chcv1  30132  hatomic  30137  atord  30165  atcvat2  30166  mddmdin0i  30208  opreu2reuALT  30240  rmoxfrd  30257  ifeqeqx  30297  ssiun2sf  30311  ssrelf  30366  fmptcof2  30402  acunirnmpt  30404  acunirnmpt2  30405  acunirnmpt2f  30406  aciunf1lem  30407  suppovss  30426  fz1nntr  30527  nn0min  30536  fsumiunle  30545  wrdt2ind  30627  ressprs  30642  resspos  30646  toslublem  30654  tosglblem  30656  xrge0tsmsd  30692  isomnd  30702  omndadd  30707  gsumle  30725  fzto1st  30745  psgnfzto1st  30747  submarchi  30815  archirng  30817  archiexdiv  30819  archiabllem1a  30820  archiabllem2a  30823  archiabl  30827  gsumvsca1  30854  gsumvsca2  30855  isorng  30872  orngmul  30876  isarchiofld  30890  linds2eq  30941  isprmidl  30955  prmidl  30957  prmidlc  30964  ismxidl  30971  mxidlmax  30974  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  submateq  31074  lmatfval  31079  lmatcl  31081  iscref  31108  crefi  31111  pcmplfin  31124  xrge0iifiso  31178  esumcvg  31345  esum2dlem  31351  sigaclcu  31376  sigaclci  31391  unelsiga  31393  unelldsys  31417  sigapildsys  31421  ldgenpisyslem1  31422  fiunelros  31433  measvun  31468  measiun  31477  carsgmon  31572  carsgsigalem  31573  carsgclctunlem2  31577  carsgclctun  31579  pmeasmono  31582  pmeasadd  31583  sibfof  31598  sitgclg  31600  eulerpartlemgvv  31634  signsply0  31821  signstfvneq0  31842  breprexp  31904  hgt749d  31920  istrkg2d  31937  axtgupdim2ALTV  31939  bnj1385  32104  bnj110  32130  bnj222  32155  bnj229  32156  bnj590  32182  bnj865  32195  bnj849  32197  bnj981  32222  bnj1014  32233  bnj1015  32234  bnj1112  32255  bnj1118  32256  bnj1123  32258  bnj1128  32262  bnj1125  32264  bnj1148  32268  bnj1154  32271  bnj1326  32298  bnj1384  32304  bnj1489  32328  bnj1497  32332  funen1cnv  32357  f1resfz0f1d  32361  cplgredgex  32367  acycgrcycl  32394  subfacp1lem6  32432  erdszelem9  32446  kur14lem9  32461  sconnpht  32476  cvmsss2  32521  cvmliftlem7  32538  cvmliftlem10  32541  fmlasuc  32633  gonar  32642  goalr  32644  mclsrcl  32808  mclsssvlem  32809  mclsval  32810  mclsax  32816  mclsind  32817  mclsppslem  32830  iota5f  32955  dfpo2  32991  fununiq  33012  setinds  33023  dfon2lem3  33030  dfon2lem4  33031  dfon2lem5  33032  dfon2lem6  33033  dfon2lem7  33034  dfon2lem8  33035  dfon2  33037  tfisg  33055  frpoinsg  33081  frmin  33084  frinsg  33087  noprefixmo  33202  nosupdm  33204  nosupfv  33206  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2  33216  nocvxminlem  33247  btwnconn1lem11  33558  linethru  33614  fwddifnp1  33626  rankelg  33629  rankeq1o  33632  subtr  33662  subtr2  33663  trer  33664  nn0prpwlem  33670  nn0prpw  33671  neibastop2lem  33708  filnetlem4  33729  bj-hbxfrbi  33963  bj-hbyfrbi  33964  bj-ssblem1  33987  bj-ssblem2  33988  bj-ax12  33990  relowlssretop  34647  rdgeqoa  34654  rdgssun  34662  exrecfnlem  34663  finxpreclem6  34680  pibp19  34698  pibt2  34701  wl-mo3t  34827  wl-sb8mot  34829  finixpnum  34892  matunitlindflem1  34903  ptrest  34906  poimirlem13  34920  poimirlem14  34921  poimirlem17  34924  poimirlem18  34925  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem28  34935  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  poimir  34940  heicant  34942  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  itg2addnclem3  34960  ftc1cnnc  34981  ftc1anclem7  34988  ftc1anc  34990  sdclem2  35032  fdc  35035  fdc1  35036  neificl  35043  mettrifi  35047  sstotbnd2  35067  cntotbnd  35089  heibor1lem  35102  bfp  35117  isass  35139  ismgmOLD  35143  isexid2  35148  iscringd  35291  ispridl  35327  pridl  35330  ismaxidl  35333  maxidlmax  35336  ispridlc  35363  pridlc  35364  dmnnzd  35368  relcnveq2  35595  ecin0  35621  elrelscnveq2  35748  elsymrels3  35805  eltrrels3  35831  eleqvrels3  35843  eqvrelqsel  35866  axc11n-16  36089  ax12eq  36092  ax12el  36093  ax12inda  36099  ax12v2-o  36100  fsumshftd  36103  riotasv2d  36108  lshpdisj  36138  lsmsatcv  36161  lsat0cv  36184  lcvexchlem4  36188  lcvexchlem5  36189  l1cvpat  36205  isopos  36331  oposlem  36333  isoml  36389  omllaw  36394  isatl  36450  atlex  36467  iscvlat  36474  cvlexch1  36479  glbconN  36528  hlsuprexch  36532  ps-1  36628  3atlem5  36638  psubspi  36898  llnexchb2  37020  elpcliN  37044  pclfinclN  37101  ldilval  37264  ltrnfset  37268  ltrnset  37269  ltrnu  37272  trlfset  37311  trlset  37312  trlval2  37314  cdleme25cv  37509  cdleme31so  37530  cdleme31fv  37541  cdlemefrs29bpre0  37547  cdleme32fva  37588  cdleme40v  37620  trlord  37720  cdlemkid3N  38084  cdlemkid4  38085  dihffval  38381  dihfval  38382  dihval  38383  lpolconN  38638  mapdordlem2  38788  hdmapfval  38978  hdmapval  38979  hdmapval2  38983  nnn1suc  39179  ismrcd1  39315  ismrcd2  39316  ismrc  39318  isnacs3  39327  nacsfix  39329  mzpcompact2  39369  fphpd  39433  fphpdo  39434  monotuz  39558  monotoddzzfi  39559  monotoddzz  39560  oddcomabszz  39561  zindbi  39563  setindtrs  39642  dford3lem2  39644  ttac  39653  dnnumch1  39664  fnwe2lem2  39671  aomclem3  39676  aomclem6  39679  aomclem8  39681  dfac11  39682  dfac21  39686  islssfg2  39691  hbtlem5  39748  hbt  39750  flcidc  39794  mendlmod  39813  rababg  39953  elmapintrab  39956  iunrelexpuztr  40084  frege92  40321  frege104  40333  ntrkbimka  40408  ntrk0kbimka  40409  neik0pk1imk0  40417  isotone1  40418  isotone2  40419  ntrclsiso  40437  ntrclskb  40439  ntrneiiso  40461  ntrneik3  40466  ntrneix3  40467  gneispacess2  40516  grur1cld  40588  scottabf  40596  ismnu  40617  mnuop23d  40622  mnuunid  40633  dvgrat  40664  cvgdvgrat  40665  binomcxplemnotnn0  40708  pm14.122b  40775  sbiota1  40786  fnchoice  41306  fiiuncl  41347  iunincfi  41380  disjf1  41463  wessf1ornlem  41465  disjinfi  41474  axccdom  41507  dmrelrnrel  41510  axccd  41515  monoords  41584  fperiodmullem  41590  supxrgere  41621  supxrgelem  41625  supxrge  41626  xrlexaddrp  41640  infxr  41655  infleinf  41660  supxrleubrnmptf  41747  monoordxrv  41778  monoordxr  41779  monoord2xr  41781  fsumclf  41870  fsummulc1f  41871  fsumnncl  41872  fsumsplit1  41873  fsumf1of  41875  fsumreclf  41877  fsumlessf  41878  fsumsermpt  41880  fmul01  41881  fmulcl  41882  fmuldfeqlem1  41883  fmuldfeq  41884  fmul01lt1lem1  41885  fmul01lt1lem2  41886  fprodexp  41895  fprodabs2  41896  fprodcnlem  41900  climmulf  41905  climexp  41906  climsuse  41909  climrecf  41910  climinff  41912  climaddf  41916  mullimc  41917  mullimcf  41924  limcperiod  41929  sumnnodd  41931  lptre2pt  41941  limsupre  41942  neglimc  41948  addlimc  41949  0ellimcdiv  41950  limclner  41952  climsubmpt  41961  climreclf  41965  climeldmeqmpt  41969  climfveqmpt  41972  fnlimfvre  41975  climfveqf  41981  climfveqmpt3  41983  climeldmeqf  41984  limsupref  41986  limsupbnd1f  41987  climeqf  41989  climeldmeqmpt3  41990  climinf2  42008  limsupubuz  42014  climinf2mpt  42015  climinfmpt  42016  limsupmnf  42022  limsupequz  42024  limsupre2  42026  limsupequzmptf  42032  limsupre3  42034  lmbr3  42048  cnrefiisp  42131  xlimxrre  42132  xlimmnfvlem1  42133  xlimpnfvlem1  42137  climxlim2lem  42146  cncfshift  42177  cncfperiod  42182  icccncfext  42190  fprodcncf  42204  fperdvper  42223  dvmptmulf  42242  dvnmptdivc  42243  dvnmul  42248  dvmptfprod  42250  dvnprodlem1  42251  dvnprodlem2  42252  dvnprodlem3  42253  iblspltprt  42278  itgspltprt  42284  stoweidlem3  42308  stoweidlem4  42309  stoweidlem6  42311  stoweidlem8  42313  stoweidlem15  42320  stoweidlem16  42321  stoweidlem17  42322  stoweidlem19  42324  stoweidlem20  42325  stoweidlem22  42327  stoweidlem23  42328  stoweidlem26  42331  stoweidlem27  42332  stoweidlem30  42335  stoweidlem31  42336  stoweidlem32  42337  stoweidlem34  42339  stoweidlem35  42340  stoweidlem42  42347  stoweidlem43  42348  stoweidlem48  42353  stoweidlem50  42355  stoweidlem51  42356  stoweidlem57  42362  stoweidlem59  42364  stoweidlem62  42367  wallispilem3  42372  dirkercncflem2  42409  fourierdlem11  42423  fourierdlem12  42424  fourierdlem15  42427  fourierdlem16  42428  fourierdlem21  42433  fourierdlem34  42446  fourierdlem41  42453  fourierdlem42  42454  fourierdlem46  42457  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem51  42462  fourierdlem68  42479  fourierdlem71  42482  fourierdlem72  42483  fourierdlem73  42484  fourierdlem76  42487  fourierdlem79  42490  fourierdlem81  42492  fourierdlem83  42494  fourierdlem86  42497  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem92  42503  fourierdlem94  42505  fourierdlem97  42508  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  fourierdlem112  42523  fourierdlem113  42524  etransclem2  42541  etransclem46  42585  salunicl  42621  saluncl  42622  intsaluni  42632  dfsalgen2  42644  sge0f1o  42684  sge0lempt  42712  sge0iunmptlemfi  42715  sge0p1  42716  sge0fodjrnlem  42718  sge0iunmpt  42720  sge0ltfirpmpt2  42728  sge0isummpt2  42734  sge0xaddlem2  42736  sge0xadd  42737  nnfoctbdjlem  42757  meadjuni  42759  meadjiun  42768  voliunsge0lem  42774  meaiuninclem  42782  meaiunincf  42785  meaiuninc3v  42786  meaiuninc3  42787  meaiininclem  42788  meaiininc  42789  omeunile  42807  isomenndlem  42832  ovn0lem  42867  ovnsubaddlem1  42872  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  hoidmvle  42902  hspmbllem2  42929  hoimbl2  42967  vonhoire  42974  vonicclem2  42986  vonn0ioo2  42992  vonn0icc2  42994  salpreimagelt  43006  salpreimalegt  43008  pimdecfgtioc  43013  pimincfltioc  43014  pimincfltioo  43016  salpreimagtge  43022  salpreimaltle  43023  salpreimagtlt  43027  incsmf  43039  decsmf  43063  smflimlem1  43067  smflimlem2  43068  smflimlem3  43069  smflimlem4  43070  smfpimcclem  43101  funressnmo  43301  aiota0def  43314  euoreqb  43328  2reu8i  43332  2reuimp0  43333  funressndmafv2rn  43442  funressnbrafv2  43463  funbrafv2  43466  smonoord  43551  elsetpreimafvbi  43571  iccpartgt  43607  iccelpart  43613  iccpartiun  43614  icceuelpartlem  43615  icceuelpart  43616  iccpartnel  43618  fargshiftf1  43621  ichexmpl2  43652  ichnreuop  43654  ichreuopeq  43655  sprsymrelfolem2  43675  prproropf1olem4  43688  paireqne  43693  reupr  43704  reuopreuprim  43708  fmtnofac2  43751  fmtnofac1  43752  prmdvdsfmtnof1lem2  43767  perfectALTVlem2  43907  nfermltl8rev  43927  nfermltl2rev  43928  sbgoldbwt  43962  sbgoldbst  43963  sgoldbeven3prm  43968  sbgoldbm  43969  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  evengpop3  43983  evengpoap3  43984  bgoldbnnsum3prm  43989  bgoldbtbndlem4  43993  bgoldbtbnd  43994  tgblthelfgott  44000  tgoldbach  44002  isomuspgrlem2b  44014  ply1mulgsumlem2  44461  islininds  44521  linindslinci  44523  lindslinindsimp1  44532  linds0  44540  lindsrng01  44543  snlindsntorlem  44545  snlindsntor  44546  ldepsnlinc  44583  nn0sumshdiglemA  44699  nn0sumshdiglemB  44700  nn0sumshdiglem1  44701  nn0sumshdiglem2  44702  nn0sumshdig  44703  itschlc0yqe  44767  bnd2d  44804  setrec1lem1  44810  setrec1lem4  44813  setrec2fun  44815