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  1847  nfbidv  1919  sbjust  2064  nfbidf  2222  drnf1v  2385  drnf1  2461  mo4  2646  axextg  2795  ralcom2  3363  raleqbidv  3401  cbvralfw  3437  cbvralf  3439  cbvralvw  3449  cbvraldva2  3456  vtoclgaf  3572  vtoclga  3573  vtocl2gaf  3575  vtocl3gaf  3576  vtocl4ga  3579  rspct  3608  rspc  3610  rspc2gv  3631  rexraleqim  3639  ralab2  3687  ralab2OLD  3688  nelrdva  3695  mob2  3705  mob  3707  morex  3709  reu7  3722  reu8  3723  reu2eqd  3726  cdeqim  3763  sbcimg  3819  csbhypf  3910  cbvralcsf  3924  dfss2f  3957  reusngf  4605  rexreusng  4610  reuprg0  4631  elpreqpr  4790  elintab  4879  intss1  4883  intmin  4888  dfiin2g  4949  trel  5171  zfpow  5259  reusv2lem4  5293  reusv3i  5296  rext  5332  opth  5360  copsexgw  5373  copsexg  5374  poeq1  5471  pocl  5475  swopolem  5477  swopo  5478  isso2i  5502  fri  5511  vtoclr  5609  poinxp  5626  posn  5631  ssrel  5651  ssrel2  5653  ssrelrel  5663  relop  5715  reu3op  6137  reuop  6138  predbrg  6162  preddowncl  6169  wfisg  6177  ordelord  6207  iota5  6332  sbcfung  6373  funopg  6383  brprcneu  6656  tz6.12f  6688  funbrfv  6710  ssimaexg  6743  fvmptf  6783  fvelrn  6838  fprg  6911  dff13f  7008  f1veqaeq  7009  fpropnf1  7019  nf1const  7053  soisores  7074  soisoi  7075  isofrlem  7087  isopolem  7092  weniso  7101  riota5f  7136  imbrov2fvoveq  7175  oprabidw  7181  oprabid  7182  f1opr  7204  ovmpos  7292  ov2gf  7293  ov3  7305  caovcan  7346  caovordig  7347  caofrss  7436  caoftrn  7438  tfis  7563  tfisi  7567  tfindsg  7569  tfindsg2  7570  tfindes  7571  dfom2  7576  limomss  7579  nnlim  7587  findsg  7603  findes  7606  f1oweALT  7667  dfoprab4f  7748  offval22  7777  f1o2ndf1  7812  frxp  7814  poxp  7816  suppfnss  7849  wfrdmcl  7957  onfununi  7972  smoel  7991  smogt  7998  tfrlem1  8006  tz7.48lem  8071  tz7.49  8075  oawordeu  8175  omordi  8186  oeordi  8207  nnmordi  8251  omabs  8268  nneob  8273  omsmolem  8274  qsel  8370  eroveu  8386  ecopovtrn  8394  ixpsnf1o  8496  fundmeng  8578  sbth  8631  limensuc  8688  nneneq  8694  php  8695  php2  8696  unxpdom  8719  pssnn  8730  findcard  8751  findcard2  8752  findcard2d  8754  findcard3  8755  ac6sfi  8756  frfi  8757  domunfican  8785  fiint  8789  iunfi  8806  finsschain  8825  dffi3  8889  marypha1lem  8891  marypha1  8892  supeq3  8907  supeq123d  8908  supmo  8910  suplub  8918  supisolem  8931  eqinf  8942  infval  8944  infmo  8953  ordiso2  8973  ordtypelem7  8982  wemaplem1  9004  wemaplem2  9005  zfregcl  9052  inf0  9078  inf3lem1  9085  zfinf  9096  axinf2  9097  dfom3  9104  elom3  9105  cantnfval2  9126  cantnfle  9128  cantnflt  9129  cantnfp1lem3  9137  oemapvali  9141  cantnflem1c  9144  cantnflem1  9146  cantnf  9150  wemapwe  9154  cnfcom  9157  setind  9170  r1sdom  9197  r1ordg  9201  rankonidlem  9251  rankunb  9273  bnd2  9316  infxpenlem  9433  infxpenc2  9442  dfac8alem  9449  dfac8clem  9452  indcardi  9461  alephordi  9494  alephinit  9515  alephfp  9528  aceq3lem  9540  dfac5lem4  9546  dfac5  9548  dfac2b  9550  dfac9  9556  dfac12lem2  9564  dfac12lem3  9565  kmlem1  9570  kmlem4  9573  kmlem10  9579  kmlem12  9581  kmlem13  9582  pwsdompw  9620  ackbij1lem16  9651  cfslb2n  9684  cfsmolem  9686  sornom  9693  fin2i  9711  infpssrlem4  9722  isfin2-2  9735  isfin3ds  9745  fin23lem17  9754  fin23lem32  9760  fin23lem34  9762  fin23lem35  9763  fin23lem39  9766  fin23lem41  9768  isf32lem2  9770  isf33lem  9782  isf34lem4  9793  isf34lem6  9796  fin1a2lem10  9825  axcc2lem  9852  axcc3  9854  axcc4dom  9857  dominf  9861  axdc2lem  9864  axdc3lem2  9867  ac6sg  9904  zorn2lem7  9918  zornn0g  9921  ttukeylem5  9929  ttukeylem6  9930  axdclem  9935  fodomg  9939  dominfac  9989  axrepndlem1  10008  axrepndlem2  10009  axunndlem1  10011  axunnd  10012  axpowndlem2  10014  axpowndlem3  10015  axpowndlem4  10016  axregndlem2  10019  axregnd  10020  axinfndlem1  10021  axinfnd  10022  axacndlem4  10026  axacndlem5  10027  axacnd  10028  zfcndpow  10032  zfcndinf  10034  fpwwe2lem5  10050  fpwwe2lem8  10053  fpwwe2lem12  10057  pwfseqlem4a  10077  pwfseqlem4  10078  pwfseqlem5  10079  pwfseq  10080  wunfi  10137  wunex2  10154  inar1  10191  rankcf  10193  tskord  10196  grudomon  10233  grur1a  10235  axgroth6  10244  axgroth3  10247  axgroth4  10248  eltskm  10259  indpi  10323  pinq  10343  nqereu  10345  prcdnq  10409  prnmax  10411  ltsopr  10448  prlem936  10463  ltsosr  10510  recexsrlem  10519  mulgt0sr  10521  map2psrpr  10526  supsrlem  10527  axrrecex  10579  axpre-lttrn  10582  axpre-mulgt0  10584  axpre-sup  10585  axsup  10710  dedekind  10797  ltordlem  11159  ltord1  11160  wloglei  11166  squeeze0  11537  infm3  11594  nnsub  11675  nnunb  11887  peano5uzti  12066  fzind  12074  eluzadd  12267  eluzsub  12268  uzind4s  12302  uzind4s2  12303  zmax  12339  zbtwnre  12340  xmulasslem  12672  xrsupsslem  12694  xrinfmsslem  12695  xrub  12699  infmremnf  12730  injresinj  13152  om2uzlti  13312  uzindi  13344  axdc4uz  13346  ssnn0fi  13347  rabssnn0fi  13348  suppssfz  13356  seqp1  13378  seqcl2  13382  seqfveq2  13386  seqshft2  13390  monoord  13394  seqsplit  13397  seqf1olem2  13404  seqf1o  13405  seqid2  13410  seqhomo  13411  seqof2  13422  expcl2lem  13435  facdiv  13641  facwordi  13643  faclbnd4lem2  13648  hashnn0n0nn  13746  hashf1lem2  13808  seqcoll  13816  fi1uzind  13849  brfi1indALT  13852  wrdind  14078  wrd2ind  14079  swrdccatin1  14081  swrdccat3blem  14095  reuccatpfxs1lem  14102  repswccat  14142  cshf1  14166  trclfvcotr  14363  relexprelg  14391  rtrclreclem4  14414  relexpindlem  14416  ello1mpt  14872  o1co  14937  o1compt  14938  rlimcn2  14941  climcn2  14943  subcn2  14945  o1of2  14963  fsumsplitf  15092  fsum2d  15120  modfsummod  15143  fsumabs  15150  telfsumo  15151  fsumrlim  15160  fsumo1  15161  o1fsum  15162  fsumiun  15170  prodfdiv  15246  fprod2d  15329  fproddivf  15335  fprodsplitf  15336  fprodsplit1f  15338  rpnnen2lem10  15570  sqrt2irr  15596  dvdsle  15654  divalglem7  15744  divalglem8  15745  ndvdssub  15754  gcdcllem1  15842  dfgcd2  15888  algcvg  15914  algcvga  15917  algfx  15918  lcmgcdlem  15944  lcmdvds  15946  lcmf  15971  lcmfunsnlem1  15975  lcmfunsnlem2lem1  15976  lcmfunsnlem  15979  lcmfdvds  15980  lcmfun  15983  coprmgcdb  15987  coprmdvds1  15990  coprmdvds2  15992  coprmprod  15999  coprmproddvds  16001  prmind2  16023  dvdsprime  16025  nprm  16026  dvdsprm  16041  exprmfct  16042  coprm  16049  isprm6  16052  prmfac1  16057  eulerthlem2  16113  pcqmul  16184  pcqcl  16187  pc2dvds  16209  pcz  16211  prmpwdvds  16234  infpn2  16243  vdwlem12  16322  ramub2  16344  rami  16345  ramcl  16359  prmdvdsprmop  16373  prmlem0  16433  mreintcl  16860  ismred2  16868  mrissmrcd  16905  mreexexlemd  16909  iscatd2  16946  moni  17000  yoniso  17529  isprs  17534  prslem  17535  drsdirfi  17542  ispos  17551  posi  17554  isposd  17559  lubfval  17582  lublecllem  17592  glbfval  17595  joinle  17618  meetle  17632  lubl  17724  lubun  17727  clatleglb  17730  pospropd  17738  poslubmo  17750  posglbmo  17751  ipodrsima  17769  acsdrsel  17771  isacs4lem  17772  isacs5lem  17773  acsdrscl  17774  mreclatBAD  17791  pslem  17810  dirtr  17840  mndind  17986  mhmlem  18213  isnsg2  18302  ghmf1  18381  orbsta  18437  symgextf1  18543  gsmsymgrfix  18550  gsmsymgreq  18554  symggen  18592  psgnunilem4  18619  sylow1lem1  18717  sylow2alem2  18737  sylow2a  18738  lsmmod  18795  lsmdisj2  18802  efgsrel  18854  efgredlemd  18864  efgredlem  18867  efgred  18868  gsumzaddlem  19035  gsummptnn0fz  19100  gsummptnn0fzfv  19101  telgsumfzs  19103  telgsums  19107  dprdval  19119  dprddisj2  19155  ablfac1eulem  19188  pgpfac1lem1  19190  pgpfac1lem5  19195  pgpfac1  19196  pgpfaclem2  19198  pgpfac  19200  irredmul  19453  f1rhm0to0ALT  19488  isdrngrd  19522  sdrgacs  19574  islbs3  19921  rrgval  20054  rrgeq0i  20056  isdomn  20061  domneq0  20064  mplsubglem  20208  mpllsslem  20209  mplcoe1  20240  mplcoe5  20243  mpfind  20314  coe1fzgsumd  20464  gsummoncoe1  20466  pf1ind  20512  evl1gsumd  20514  prmirredlem  20634  znfld  20701  znrrg  20706  cygznlem3  20710  isphl  20766  ipeq0  20776  isphld  20792  phlpropd  20793  lsmcss  20830  frlmphl  20919  frlmup1  20936  lindfrn  20959  islindf4  20976  islindf5  20977  dmatelnd  21099  mat1scmat  21142  mdetdiaglem  21201  mdetralt  21211  mdetralt2  21212  mdetunilem1  21215  mdetunilem2  21216  mdetunilem3  21217  mdetunilem4  21218  mdetunilem9  21223  smadiadetr  21278  pmatcoe1fsupp  21303  mp2pm2mplem4  21411  uniopn  21499  fiinopn  21503  epttop  21611  clsndisj  21677  elcls3  21685  neiptoptop  21733  neiptopnei  21734  cnpval  21838  iscnp  21839  cnpimaex  21858  lmcvg  21864  cnprest  21891  cnprest2  21892  lmss  21900  lmff  21903  t0sep  21926  hausnei  21930  isnrm2  21960  t1sep2  21971  isreg2  21979  iscmp  21990  cmpcov  21991  cmpsublem  22001  cmpsub  22002  tgcmp  22003  uncmp  22005  fiuncmp  22006  hauscmplem  22008  cmpfi  22010  cmpfii  22011  dfconn2  22021  connsuba  22022  connsub  22023  nconnsubb  22025  1stcclb  22046  1stcfb  22047  2ndc1stc  22053  1stcrest  22055  1stcelcls  22063  restnlly  22084  lly1stc  22098  comppfsc  22134  kgenval  22137  kgeni  22139  kgencn2  22159  ptcldmpt  22216  ptclsg  22217  dfac14lem  22219  dfac14  22220  txcnp  22222  ptcnp  22224  hausdiag  22247  txlm  22250  tx1stc  22252  xkococn  22262  cnmpt12  22269  cnmpt22  22276  kqt0lem  22338  isr0  22339  regr1lem2  22342  kqreglem1  22343  r0sep  22350  ptcmpfi  22415  elmptrab  22429  isfil  22449  filss  22455  isufil2  22510  cfinufil  22530  rnelfm  22555  fmfnfmlem2  22557  fmfnfmlem4  22559  flimopn  22577  flimrest  22585  flftg  22598  cnpflf  22603  txflf  22608  fclsopni  22617  fclsrest  22626  fclscf  22627  flimfnfcls  22630  fcfnei  22637  alexsublem  22646  alexsubb  22648  alexsubALTlem3  22651  alexsubALTlem4  22652  alexsubALT  22653  cnextcn  22669  cnextfres1  22670  tgpt0  22721  qustgplem  22723  tsmsi  22736  tsmssubm  22745  tsmsres  22746  tsmsf1o  22747  tsmsxp  22757  ustssel  22808  ust0  22822  ustuqtop4  22847  ucnima  22884  ucncn  22888  iscusp  22902  cuspcvg  22904  imasdsf1olem  22977  blssps  23028  blss  23029  metss  23112  comet  23117  metcnp3  23144  metcnp2  23146  txmetcnp  23151  metuel2  23169  metucn  23175  nrmmetd  23178  nlmvscn  23290  nrginvrcn  23295  nmolb  23320  xrge0tsms  23436  divcn  23470  fsumcn  23472  elcncf2  23492  cncfi  23496  mulc1cncf  23507  cncfmet  23510  xrhmeo  23544  bndth  23556  nmoleub2lem2  23714  nmoleub3  23717  ipcn  23843  lmmbr  23855  caucfil  23880  pmltpc  24045  ovolfiniun  24096  ovolicc2lem3  24114  ovolicc2  24117  mblsplit  24127  finiunmbl  24139  volfiniun  24142  voliunlem3  24147  ioorinv  24171  ioorcl  24172  dyadmax  24193  dyadmbllem  24194  dyadmbl  24195  opnmbllem  24196  volcn  24201  vitalilem2  24204  vitalilem3  24205  vitali  24208  i1fd  24276  itg2seq  24337  itg2addlem  24353  itgfsum  24421  ellimc3  24471  dvbsss  24494  dvnres  24522  dvmptfsum  24566  dvferm1lem  24575  dvferm2lem  24577  rolle  24581  c1lip1  24588  lhop1lem  24604  lhop1  24605  dvfsumlem2  24618  dvfsumlem4  24620  dvfsumrlim  24622  dvfsum2  24625  ftc1a  24628  ftc1lem6  24632  mdegleb  24652  mdeglt  24653  deg1leb  24683  deg1lt  24685  ply1divex  24724  fta1glem2  24754  fta1g  24755  plyco0  24776  plyeq0lem  24794  coeeq2  24826  dgrle  24827  dgrcolem2  24858  dgrco  24859  plydivlem4  24879  plydivex  24880  fta1lem  24890  fta1  24891  vieta1lem2  24894  vieta1  24895  aalioulem2  24916  aalioulem4  24918  abelth  25023  cxpcn3  25323  rlimcnp  25537  xrlimcnp  25540  cxploglim  25549  scvxcvx  25557  jensen  25560  lgamgulmlem2  25601  wilthlem2  25640  wilthlem3  25641  fta  25651  dvdsmulf1o  25765  perfectlem2  25800  dchrelbas3  25808  dchrelbas4  25813  dchrn0  25820  bcmono  25847  lgsdir2lem4  25898  lgsdchr  25925  gausslemma2dlem0i  25934  lgseisenlem2  25946  lgsquad2lem2  25955  2sqlem6  25993  2sqlem8  25996  2sqlem10  25998  dchrisumlema  26058  dchrisumlem2  26060  dchrisumlem3  26061  istrkgb  26235  istrkgcb  26236  istrkge  26237  axtgcgrid  26243  axtg5seg  26245  axtgbtwnid  26246  axtgpasch  26247  axtgcont1  26248  axtgeucl  26252  iscgrglt  26294  tgcgr4  26311  axcgrtr  26695  gropd  26810  grstructd  26811  upgredg2vtx  26920  upgredgpr  26921  edglnl  26922  numedglnl  26923  usgredg2vtxeuALT  26998  nbgr2vtx1edg  27126  finsumvtxdg2size  27326  wlkp1lem8  27456  upgrwlkdvdelem  27511  usgr2wlkneq  27531  usgr2pthlem  27538  pthdlem2lem  27542  uspgrn2crct  27580  2pthdlem1  27703  eleclclwwlkn  27849  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  3pthdlem1  27937  eupth2  28012  frgr3vlem1  28046  3vfriswmgrlem  28050  frgrwopreglem4a  28083  frgr2wwlk1  28102  wlkl0  28140  numclwlk2lem2f1o  28152  friendshipgt3  28171  eulplig  28256  nvz  28440  nmobndseqi  28550  nmobndseqiALT  28551  nmlno0  28566  blocnilem  28575  dipdir  28613  dipass  28616  siilem2  28623  ubthlem2  28642  ubth  28644  htth  28689  normpyth  28916  norm3lemt  28923  chlimi  29005  chcompl  29013  omlsii  29174  pjoml  29207  h1de2i  29324  elspansn2  29338  h1datom  29353  pjoml2  29382  pjoml3  29383  lecm  29388  chscllem2  29409  osum  29416  spansncv  29424  pjcjt2  29463  pjopyth  29491  eigre  29606  eigorth  29609  hhcno  29675  hhcnf  29676  cnopc  29684  cnfnc  29701  nmcexi  29797  nmcopexi  29798  nmcfnexi  29822  pjssge0i  29937  hstel2  29990  stj  30006  stri  30028  hstri  30036  stcltr1i  30045  mdbr  30065  mdi  30066  mdbr3  30068  mdbr4  30069  dmdbr  30070  dmdmd  30071  dmdi  30073  dmdbr3  30076  dmdbr4  30077  dmdbr5  30079  mdsl1i  30092  mdslmd1lem3  30098  mdslmd1lem4  30099  mdslmd1i  30100  csmdsymi  30105  cvmd  30107  atss  30117  atom1d  30124  chcv1  30126  hatomic  30131  atord  30159  atcvat2  30160  mddmdin0i  30202  opreu2reuALT  30234  rmoxfrd  30251  ifeqeqx  30291  ssiun2sf  30305  ssrelf  30360  fmptcof2  30396  acunirnmpt  30398  acunirnmpt2  30399  acunirnmpt2f  30400  aciunf1lem  30401  suppovss  30420  fz1nntr  30521  nn0min  30531  fsumiunle  30540  wrdt2ind  30622  ressprs  30637  resspos  30641  toslublem  30649  tosglblem  30651  xrge0tsmsd  30687  isomnd  30697  omndadd  30702  gsumle  30720  fzto1st  30740  psgnfzto1st  30742  submarchi  30810  archirng  30812  archiexdiv  30814  archiabllem1a  30815  archiabllem2a  30818  archiabl  30822  gsumvsca1  30849  gsumvsca2  30850  isorng  30867  orngmul  30871  isarchiofld  30885  linds2eq  30936  isprmidl  30950  prmidl  30952  prmidlc  30959  ismxidl  30966  mxidlmax  30969  lbsdiflsp0  31017  fedgmullem1  31020  fedgmullem2  31021  submateq  31069  lmatfval  31074  lmatcl  31076  iscref  31103  crefi  31106  pcmplfin  31119  xrge0iifiso  31173  esumcvg  31340  esum2dlem  31346  sigaclcu  31371  sigaclci  31386  unelsiga  31388  unelldsys  31412  sigapildsys  31416  ldgenpisyslem1  31417  fiunelros  31428  measvun  31463  measiun  31472  carsgmon  31567  carsgsigalem  31568  carsgclctunlem2  31572  carsgclctun  31574  pmeasmono  31577  pmeasadd  31578  sibfof  31593  sitgclg  31595  eulerpartlemgvv  31629  signsply0  31816  signstfvneq0  31837  breprexp  31899  hgt749d  31915  istrkg2d  31932  axtgupdim2ALTV  31934  bnj1385  32099  bnj110  32125  bnj222  32150  bnj229  32151  bnj590  32177  bnj865  32190  bnj849  32192  bnj981  32217  bnj1014  32228  bnj1015  32229  bnj1112  32250  bnj1118  32251  bnj1123  32253  bnj1128  32257  bnj1125  32259  bnj1148  32263  bnj1154  32266  bnj1326  32293  bnj1384  32299  bnj1489  32323  bnj1497  32327  funen1cnv  32352  f1resfz0f1d  32356  cplgredgex  32362  acycgrcycl  32389  subfacp1lem6  32427  erdszelem9  32441  kur14lem9  32456  sconnpht  32471  cvmsss2  32516  cvmliftlem7  32533  cvmliftlem10  32536  fmlasuc  32628  gonar  32637  goalr  32639  mclsrcl  32803  mclsssvlem  32804  mclsval  32805  mclsax  32811  mclsind  32812  mclsppslem  32825  iota5f  32950  dfpo2  32986  fununiq  33007  setinds  33018  dfon2lem3  33025  dfon2lem4  33026  dfon2lem5  33027  dfon2lem6  33028  dfon2lem7  33029  dfon2lem8  33030  dfon2  33032  tfisg  33050  frpoinsg  33076  frmin  33079  frinsg  33082  noprefixmo  33197  nosupdm  33199  nosupfv  33201  nosupres  33202  nosupbnd1lem1  33203  nosupbnd1lem3  33205  nosupbnd1lem5  33207  nosupbnd2  33211  nocvxminlem  33242  btwnconn1lem11  33553  linethru  33609  fwddifnp1  33621  rankelg  33624  rankeq1o  33627  subtr  33657  subtr2  33658  trer  33659  nn0prpwlem  33665  nn0prpw  33666  neibastop2lem  33703  filnetlem4  33724  bj-hbxfrbi  33958  bj-hbyfrbi  33959  bj-ssblem1  33982  bj-ssblem2  33983  bj-ax12  33985  relowlssretop  34638  rdgeqoa  34645  rdgssun  34653  exrecfnlem  34654  finxpreclem6  34671  pibp19  34689  pibt2  34692  wl-mo3t  34806  wl-sb8mot  34808  finixpnum  34871  matunitlindflem1  34882  ptrest  34885  poimirlem13  34899  poimirlem14  34900  poimirlem17  34903  poimirlem18  34904  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem24  34910  poimirlem25  34911  poimirlem26  34912  poimirlem28  34914  poimirlem30  34916  poimirlem31  34917  poimirlem32  34918  poimir  34919  heicant  34921  mblfinlem1  34923  mblfinlem2  34924  mblfinlem3  34925  voliunnfl  34930  volsupnfl  34931  mbfresfi  34932  itg2addnclem3  34939  ftc1cnnc  34960  ftc1anclem7  34967  ftc1anc  34969  sdclem2  35011  fdc  35014  fdc1  35015  neificl  35022  mettrifi  35026  sstotbnd2  35046  cntotbnd  35068  heibor1lem  35081  bfp  35096  isass  35118  ismgmOLD  35122  isexid2  35127  iscringd  35270  ispridl  35306  pridl  35309  ismaxidl  35312  maxidlmax  35315  ispridlc  35342  pridlc  35343  dmnnzd  35347  relcnveq2  35574  ecin0  35600  elrelscnveq2  35727  elsymrels3  35784  eltrrels3  35810  eleqvrels3  35822  eqvrelqsel  35845  axc11n-16  36068  ax12eq  36071  ax12el  36072  ax12inda  36078  ax12v2-o  36079  fsumshftd  36082  riotasv2d  36087  lshpdisj  36117  lsmsatcv  36140  lsat0cv  36163  lcvexchlem4  36167  lcvexchlem5  36168  l1cvpat  36184  isopos  36310  oposlem  36312  isoml  36368  omllaw  36373  isatl  36429  atlex  36446  iscvlat  36453  cvlexch1  36458  glbconN  36507  hlsuprexch  36511  ps-1  36607  3atlem5  36617  psubspi  36877  llnexchb2  36999  elpcliN  37023  pclfinclN  37080  ldilval  37243  ltrnfset  37247  ltrnset  37248  ltrnu  37251  trlfset  37290  trlset  37291  trlval2  37293  cdleme25cv  37488  cdleme31so  37509  cdleme31fv  37520  cdlemefrs29bpre0  37526  cdleme32fva  37567  cdleme40v  37599  trlord  37699  cdlemkid3N  38063  cdlemkid4  38064  dihffval  38360  dihfval  38361  dihval  38362  lpolconN  38617  mapdordlem2  38767  hdmapfval  38957  hdmapval  38958  hdmapval2  38962  nnn1suc  39152  ismrcd1  39288  ismrcd2  39289  ismrc  39291  isnacs3  39300  nacsfix  39302  mzpcompact2  39342  fphpd  39406  fphpdo  39407  monotuz  39531  monotoddzzfi  39532  monotoddzz  39533  oddcomabszz  39534  zindbi  39536  setindtrs  39615  dford3lem2  39617  ttac  39626  dnnumch1  39637  fnwe2lem2  39644  aomclem3  39649  aomclem6  39652  aomclem8  39654  dfac11  39655  dfac21  39659  islssfg2  39664  hbtlem5  39721  hbt  39723  flcidc  39767  mendlmod  39786  rababg  39926  elmapintrab  39929  iunrelexpuztr  40057  frege92  40294  frege104  40306  ntrkbimka  40381  ntrk0kbimka  40382  neik0pk1imk0  40390  isotone1  40391  isotone2  40392  ntrclsiso  40410  ntrclskb  40412  ntrneiiso  40434  ntrneik3  40439  ntrneix3  40440  gneispacess2  40489  grur1cld  40561  scottabf  40569  ismnu  40590  mnuop23d  40595  mnuunid  40606  dvgrat  40637  cvgdvgrat  40638  binomcxplemnotnn0  40681  pm14.122b  40748  sbiota1  40759  fnchoice  41279  fiiuncl  41320  iunincfi  41353  disjf1  41436  wessf1ornlem  41438  disjinfi  41447  axccdom  41480  dmrelrnrel  41483  axccd  41488  monoords  41557  fperiodmullem  41563  supxrgere  41594  supxrgelem  41598  supxrge  41599  xrlexaddrp  41613  infxr  41628  infleinf  41633  supxrleubrnmptf  41720  monoordxrv  41751  monoordxr  41752  monoord2xr  41754  fsumclf  41843  fsummulc1f  41844  fsumnncl  41845  fsumsplit1  41846  fsumf1of  41848  fsumreclf  41850  fsumlessf  41851  fsumsermpt  41853  fmul01  41854  fmulcl  41855  fmuldfeqlem1  41856  fmuldfeq  41857  fmul01lt1lem1  41858  fmul01lt1lem2  41859  fprodexp  41868  fprodabs2  41869  fprodcnlem  41873  climmulf  41878  climexp  41879  climsuse  41882  climrecf  41883  climinff  41885  climaddf  41889  mullimc  41890  mullimcf  41897  limcperiod  41902  sumnnodd  41904  lptre2pt  41914  limsupre  41915  neglimc  41921  addlimc  41922  0ellimcdiv  41923  limclner  41925  climsubmpt  41934  climreclf  41938  climeldmeqmpt  41942  climfveqmpt  41945  fnlimfvre  41948  climfveqf  41954  climfveqmpt3  41956  climeldmeqf  41957  limsupref  41959  limsupbnd1f  41960  climeqf  41962  climeldmeqmpt3  41963  climinf2  41981  limsupubuz  41987  climinf2mpt  41988  climinfmpt  41989  limsupmnf  41995  limsupequz  41997  limsupre2  41999  limsupequzmptf  42005  limsupre3  42007  lmbr3  42021  cnrefiisp  42104  xlimxrre  42105  xlimmnfvlem1  42106  xlimpnfvlem1  42110  climxlim2lem  42119  cncfshift  42150  cncfperiod  42155  icccncfext  42163  fprodcncf  42177  fperdvper  42196  dvmptmulf  42215  dvnmptdivc  42216  dvnmul  42221  dvmptfprod  42223  dvnprodlem1  42224  dvnprodlem2  42225  dvnprodlem3  42226  iblspltprt  42251  itgspltprt  42257  stoweidlem3  42282  stoweidlem4  42283  stoweidlem6  42285  stoweidlem8  42287  stoweidlem15  42294  stoweidlem16  42295  stoweidlem17  42296  stoweidlem19  42298  stoweidlem20  42299  stoweidlem22  42301  stoweidlem23  42302  stoweidlem26  42305  stoweidlem27  42306  stoweidlem30  42309  stoweidlem31  42310  stoweidlem32  42311  stoweidlem34  42313  stoweidlem35  42314  stoweidlem42  42321  stoweidlem43  42322  stoweidlem48  42327  stoweidlem50  42329  stoweidlem51  42330  stoweidlem57  42336  stoweidlem59  42338  stoweidlem62  42341  wallispilem3  42346  dirkercncflem2  42383  fourierdlem11  42397  fourierdlem12  42398  fourierdlem15  42401  fourierdlem16  42402  fourierdlem21  42407  fourierdlem34  42420  fourierdlem41  42427  fourierdlem42  42428  fourierdlem46  42431  fourierdlem48  42433  fourierdlem49  42434  fourierdlem50  42435  fourierdlem51  42436  fourierdlem68  42453  fourierdlem71  42456  fourierdlem72  42457  fourierdlem73  42458  fourierdlem76  42461  fourierdlem79  42464  fourierdlem81  42466  fourierdlem83  42468  fourierdlem86  42471  fourierdlem89  42474  fourierdlem90  42475  fourierdlem91  42476  fourierdlem92  42477  fourierdlem94  42479  fourierdlem97  42482  fourierdlem103  42488  fourierdlem104  42489  fourierdlem111  42496  fourierdlem112  42497  fourierdlem113  42498  etransclem2  42515  etransclem46  42559  salunicl  42595  saluncl  42596  intsaluni  42606  dfsalgen2  42618  sge0f1o  42658  sge0lempt  42686  sge0iunmptlemfi  42689  sge0p1  42690  sge0fodjrnlem  42692  sge0iunmpt  42694  sge0ltfirpmpt2  42702  sge0isummpt2  42708  sge0xaddlem2  42710  sge0xadd  42711  nnfoctbdjlem  42731  meadjuni  42733  meadjiun  42742  voliunsge0lem  42748  meaiuninclem  42756  meaiunincf  42759  meaiuninc3v  42760  meaiuninc3  42761  meaiininclem  42762  meaiininc  42763  omeunile  42781  isomenndlem  42806  ovn0lem  42841  ovnsubaddlem1  42846  hoidmvlelem2  42872  hoidmvlelem3  42873  hoidmvlelem4  42874  hoidmvle  42876  hspmbllem2  42903  hoimbl2  42941  vonhoire  42948  vonicclem2  42960  vonn0ioo2  42966  vonn0icc2  42968  salpreimagelt  42980  salpreimalegt  42982  pimdecfgtioc  42987  pimincfltioc  42988  pimincfltioo  42990  salpreimagtge  42996  salpreimaltle  42997  salpreimagtlt  43001  incsmf  43013  decsmf  43037  smflimlem1  43041  smflimlem2  43042  smflimlem3  43043  smflimlem4  43044  smfpimcclem  43075  funressnmo  43275  aiota0def  43288  euoreqb  43302  2reu8i  43306  2reuimp0  43307  funressndmafv2rn  43416  funressnbrafv2  43437  funbrafv2  43440  smonoord  43525  elsetpreimafvbi  43545  iccpartgt  43581  iccelpart  43587  iccpartiun  43588  icceuelpartlem  43589  icceuelpart  43590  iccpartnel  43592  fargshiftf1  43595  ichexmpl2  43626  ichnreuop  43628  ichreuopeq  43629  sprsymrelfolem2  43649  prproropf1olem4  43662  paireqne  43667  reupr  43678  reuopreuprim  43682  fmtnofac2  43725  fmtnofac1  43726  prmdvdsfmtnof1lem2  43741  perfectALTVlem2  43881  nfermltl8rev  43901  nfermltl2rev  43902  sbgoldbwt  43936  sbgoldbst  43937  sgoldbeven3prm  43942  sbgoldbm  43943  nnsum4primesodd  43955  nnsum4primesoddALTV  43956  evengpop3  43957  evengpoap3  43958  bgoldbnnsum3prm  43963  bgoldbtbndlem4  43967  bgoldbtbnd  43968  tgblthelfgott  43974  tgoldbach  43976  isomuspgrlem2b  43988  ply1mulgsumlem2  44435  islininds  44495  linindslinci  44497  lindslinindsimp1  44506  linds0  44514  lindsrng01  44517  snlindsntorlem  44519  snlindsntor  44520  ldepsnlinc  44557  nn0sumshdiglemA  44673  nn0sumshdiglemB  44674  nn0sumshdiglem1  44675  nn0sumshdiglem2  44676  nn0sumshdig  44677  itschlc0yqe  44741  bnd2d  44778  setrec1lem1  44784  setrec1lem4  44787  setrec2fun  44789