Theorem imbi12d 333

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  imbi12  335  nfbidf  2079  nfbidfOLD  2189  axc15  2291  drnf1  2317  ax12v2OLD  2330  mobid  2477  axext3ALT  2593  ralcom2  3083  cbvralf  3141  cbvraldva2  3151  vtoclgaf  3244  vtocl2gaf  3246  vtocl3gaf  3248  vtocl4ga  3251  rspct  3275  rspc  3276  rexraleqim  3299  ralab2  3338  mob2  3353  mob  3355  morex  3357  reu7  3368  reu8  3369  reu2eqd  3370  nelrdva  3384  cdeqim  3395  sbcimg  3444  csbhypf  3518  cbvralcsf  3531  dfss2f  3559  sneqrgOLD  4313  prel12g  4327  elpreqpr  4334  elintab  4422  intss1  4427  intmin  4432  dfiin2g  4489  trel  4687  trssOLD  4690  zfpow  4770  reusv2lem4  4798  reusv3i  4801  rext  4843  opth  4871  copsexg  4882  poeq1  4962  pocl  4966  swopolem  4968  swopo  4969  isso2i  4991  fri  5000  vtoclr  5086  poinxp  5105  posn  5110  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  relop  5194  issref  5428  predbrg  5617  preddowncl  5624  wfisg  5632  ordelord  5662  iota5  5788  sbcfung  5827  funopg  5836  brprcneu  6096  tz6.12f  6122  funbrfv  6144  ssimaexg  6174  fvmptf  6209  fvelrn  6260  fprg  6327  dff13f  6417  f1veqaeq  6418  soisores  6477  soisoi  6478  isofrlem  6490  isopolem  6495  weniso  6504  riota5f  6535  oprabid  6576  ovmpt2s  6682  ov2gf  6683  ov3  6695  caovcan  6736  caovordig  6737  caofrss  6828  caoftrn  6830  tfis  6946  tfisi  6950  tfindsg  6952  tfindsg2  6953  tfindes  6954  dfom2  6959  limomss  6962  nnlim  6970  findsg  6985  findes  6988  f1oweALT  7043  dfoprab4f  7117  offval22  7140  f1o2ndf1  7172  frxp  7174  poxp  7176  suppfnss  7207  wfrdmcl  7310  onfununi  7325  smoel  7344  smogt  7351  tfrlem1  7359  tz7.48lem  7423  tz7.49  7427  oawordeu  7522  omordi  7533  oeordi  7554  nnmordi  7598  omabs  7614  nneob  7619  omsmolem  7620  qsel  7713  eroveu  7729  ecopovtrn  7737  ixpsnf1o  7834  fundmeng  7917  sbth  7965  limensuc  8022  nneneq  8028  php  8029  php2  8030  unxpdom  8052  pssnn  8063  findcard  8084  findcard2  8085  findcard2d  8087  findcard3  8088  ac6sfi  8089  frfi  8090  domunfican  8118  fiint  8122  iunfi  8137  finsschain  8156  dffi3  8220  marypha1lem  8222  marypha1  8223  supeq3  8238  supeq123d  8239  supmo  8241  suplub  8249  supisolem  8262  eqinf  8273  infval  8275  infmo  8284  ordiso2  8303  ordtypelem7  8312  wemaplem1  8334  wemaplem2  8335  zfregcl  8382  zfregclOLD  8384  inf0  8401  inf3lem1  8408  zfinf  8419  axinf2  8420  dfom3  8427  elom3  8428  cantnfval2  8449  cantnfle  8451  cantnflt  8452  cantnfp1lem3  8460  oemapvali  8464  cantnflem1c  8467  cantnflem1  8469  cantnf  8473  wemapwe  8477  cnfcom  8480  setind  8493  r1sdom  8520  r1ordg  8524  rankonidlem  8574  rankunb  8596  bnd2  8639  infxpenlem  8719  infxpenc2  8728  dfac8alem  8735  dfac8clem  8738  indcardi  8747  alephordi  8780  alephinit  8801  alephfp  8814  aceq3lem  8826  dfac5lem4  8832  dfac5  8834  dfac2  8836  dfac9  8841  dfac12lem2  8849  dfac12lem3  8850  kmlem1  8855  kmlem4  8858  kmlem10  8864  kmlem12  8866  kmlem13  8867  pwsdompw  8909  ackbij1lem16  8940  cfslb2n  8973  cfsmolem  8975  sornom  8982  fin2i  9000  infpssrlem4  9011  isfin2-2  9024  isfin3ds  9034  fin23lem17  9043  fin23lem32  9049  fin23lem34  9051  fin23lem35  9052  fin23lem39  9055  fin23lem41  9057  isf32lem2  9059  isf33lem  9071  isf34lem4  9082  isf34lem6  9085  fin1a2lem10  9114  axcc2lem  9141  axcc3  9143  axcc4dom  9146  dominf  9150  axdc2lem  9153  axdc3lem2  9156  ac6sg  9193  zorn2lem7  9207  zornn0g  9210  ttukeylem5  9218  ttukeylem6  9219  axdclem  9224  fodomg  9228  dominfac  9274  axrepndlem1  9293  axrepndlem2  9294  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  zfcndpow  9317  zfcndinf  9319  fpwwe2lem5  9335  fpwwe2lem8  9338  fpwwe2lem12  9342  pwfseqlem4a  9362  pwfseqlem4  9363  pwfseqlem5  9364  pwfseq  9365  wunfi  9422  wunex2  9439  inar1  9476  rankcf  9478  tskord  9481  grudomon  9518  grur1a  9520  axgroth6  9529  axgroth3  9532  axgroth4  9533  eltskm  9544  indpi  9608  pinq  9628  nqereu  9630  prcdnq  9694  prnmax  9696  ltsopr  9733  prlem936  9748  ltsosr  9794  recexsrlem  9803  mulgt0sr  9805  map2psrpr  9810  supsrlem  9811  axrrecex  9863  axpre-lttrn  9866  axpre-mulgt0  9868  axpre-sup  9869  axsup  9992  dedekind  10079  ltordlem  10432  ltord1  10433  wloglei  10439  squeeze0  10805  infm3  10861  nnsub  10936  nnunb  11165  peano5uzti  11343  fzind  11351  eluzadd  11592  eluzsub  11593  uzind4s  11624  uzind4s2  11625  zmax  11661  zbtwnre  11662  xmulasslem  11987  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  infmremnf  12044  injresinj  12451  om2uzlti  12611  uzindi  12643  axdc4uz  12645  ssnn0fi  12646  rabssnn0fi  12647  suppssfz  12656  seqp1  12678  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqf1olem2  12703  seqf1o  12704  seqid2  12709  seqhomo  12710  seqof2  12721  expcl2lem  12734  facdiv  12936  facwordi  12938  faclbnd4lem2  12943  hashnn0n0nn  13041  hashf1lem2  13097  seqcoll  13105  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  wrdind  13328  wrd2ind  13329  reuccats1lem  13331  swrdccatin1  13334  swrdccat3blem  13346  repswccat  13383  cshf1  13407  trclfvcotr  13598  relexprelg  13626  rtrclreclem4  13649  relexpindlem  13651  rlim2  14075  ello1mpt  14100  rlimclim1  14124  o1co  14165  o1compt  14166  rlimcn1  14167  rlimcn2  14169  climcn1  14170  climcn2  14171  subcn2  14173  o1of2  14191  caucvgrlem  14251  fsum2d  14344  modfsummod  14367  fsumabs  14374  telfsumo  14375  fsumrlim  14384  fsumo1  14385  o1fsum  14386  fsumiun  14394  prodfdiv  14467  fprod2d  14550  fproddivf  14557  fprodsplitf  14558  fprodsplit1f  14560  rpnnen2lem10  14791  sqrt2irr  14817  dvdsle  14870  divalglem7  14960  divalglem8  14961  ndvdssub  14971  gcdcllem1  15059  dfgcd2  15101  algcvg  15127  algcvga  15130  algfx  15131  lcmgcdlem  15157  lcmdvds  15159  lcmf  15184  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem  15192  lcmfdvds  15193  lcmfun  15196  coprmgcdb  15200  coprmdvds1  15203  coprmdvds2  15206  coprmprod  15213  coprmproddvds  15215  isprm2lem  15232  prmind2  15236  dvdsprime  15238  nprm  15239  dvdsprm  15253  exprmfct  15254  coprm  15261  isprm6  15264  prmfac1  15269  eulerthlem2  15325  pcqmul  15396  pcqcl  15399  pc2dvds  15421  pcz  15423  prmpwdvds  15446  infpn2  15455  vdwlem12  15534  ramub2  15556  rami  15557  ramcl  15571  prmdvdsprmop  15585  prmlem0  15650  mreintcl  16078  ismred2  16086  mrissmrcd  16123  mreexexlemd  16127  iscatd2  16165  moni  16219  yoniso  16748  isprs  16753  prslem  16754  drsdirfi  16761  ispos  16770  posi  16773  isposd  16778  lubfval  16801  lublecllem  16811  glbfval  16814  joinle  16837  meetle  16851  lubl  16943  lubun  16946  clatleglb  16949  pospropd  16957  poslubmo  16969  posglbmo  16970  ipodrsima  16988  acsdrsel  16990  isacs4lem  16991  isacs5lem  16992  acsdrscl  16993  mreclatBAD  17010  pslem  17029  dirtr  17059  mrcmndind  17189  mhmlem  17358  isnsg2  17447  ghmf1  17512  orbsta  17569  symgextf1  17664  gsmsymgrfix  17671  gsmsymgreq  17675  symggen  17713  psgnunilem4  17740  sylow1lem1  17836  sylow2alem2  17856  sylow2a  17857  lsmmod  17911  lsmdisj2  17918  efgsrel  17970  efgredlemd  17980  efgredlem  17983  efgred  17984  gsumzaddlem  18144  gsummptnn0fz  18205  gsummptnn0fzfv  18207  telgsumfzs  18209  telgsums  18213  dprdval  18225  dprddisj2  18261  ablfac1eulem  18294  pgpfac1lem1  18296  pgpfac1lem5  18301  pgpfac1  18302  pgpfaclem2  18304  pgpfac  18306  irredmul  18532  f1rhm0to0ALT  18564  isdrngrd  18596  islbs3  18976  rrgval  19108  rrgeq0i  19110  isdomn  19115  domneq0  19118  mplsubglem  19255  mpllsslem  19256  mplcoe1  19286  mplcoe5  19289  mpfind  19357  coe1fzgsumd  19493  gsummoncoe1  19495  pf1ind  19540  evl1gsumd  19542  prmirredlem  19660  znfld  19728  znrrg  19733  cygznlem3  19737  isphl  19792  ipeq0  19802  isphld  19818  phlpropd  19819  lsmcss  19855  frlmphl  19939  frlmup1  19956  lindfrn  19979  islindf4  19996  islindf5  19997  dmatelnd  20121  mat1scmat  20164  mdetdiaglem  20223  mdetralt  20233  mdetralt2  20234  mdetunilem1  20237  mdetunilem2  20238  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  smadiadetr  20300  pmatcoe1fsupp  20325  mp2pm2mplem4  20433  uniopn  20527  fiinopn  20531  epttop  20623  clsndisj  20689  elcls3  20697  neiptoptop  20745  neiptopnei  20746  cnpval  20850  iscnp  20851  cnpimaex  20870  lmcvg  20876  cnprest  20903  cnprest2  20904  lmss  20912  lmff  20915  ist1  20935  t0sep  20938  hausnei  20942  isnrm2  20972  t1sep2  20983  isreg2  20991  iscmp  21001  cmpcov  21002  cmpsublem  21012  cmpsub  21013  tgcmp  21014  uncmp  21016  fiuncmp  21017  hauscmplem  21019  cmpfi  21021  cmpfii  21022  dfcon2  21032  consuba  21033  connsub  21034  nconsubb  21036  1stcclb  21057  1stcfb  21058  2ndc1stc  21064  1stcrest  21066  1stcelcls  21074  restnlly  21095  lly1stc  21109  comppfsc  21145  kgenval  21148  kgeni  21150  kgencn2  21170  ptcldmpt  21227  ptclsg  21228  dfac14lem  21230  dfac14  21231  txcnp  21233  ptcnp  21235  hausdiag  21258  txlm  21261  tx1stc  21263  xkococn  21273  cnmpt12  21280  cnmpt22  21287  kqt0lem  21349  isr0  21350  regr1lem2  21353  kqreglem1  21354  r0sep  21361  ptcmpfi  21426  elmptrab  21440  isfil  21461  filss  21467  isufil2  21522  cfinufil  21542  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  flimopn  21589  flimrest  21597  flftg  21610  cnpflf  21615  txflf  21620  fclsopni  21629  fclsrest  21638  fclscf  21639  flimfnfcls  21642  fcfnei  21649  alexsublem  21658  alexsubb  21660  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  cnextcn  21681  cnextfres1  21682  tgpt0  21732  qustgplem  21734  tsmsi  21747  tsmssubm  21756  tsmsres  21757  tsmsf1o  21758  tsmsxp  21768  ustssel  21819  ust0  21833  ustuqtop4  21858  ucnima  21895  ucncn  21899  iscusp  21913  cuspcvg  21915  imasdsf1olem  21988  blssps  22039  blss  22040  metss  22123  comet  22128  metcnp3  22155  metcnp2  22157  txmetcnp  22162  metuel2  22180  metucn  22186  nrmmetd  22189  nlmvscn  22301  nrginvrcn  22306  nmolb  22331  xrge0tsms  22445  divcn  22479  fsumcn  22481  elcncf2  22501  cncfi  22505  mulc1cncf  22516  cncfco  22518  cncfmet  22519  xrhmeo  22553  bndth  22565  nmoleub2lem2  22724  nmoleub3  22727  ipcn  22853  lmmbr  22864  caucfil  22889  pmltpc  23026  ovolfiniun  23076  ovolicc2lem3  23094  ovolicc2  23097  mblsplit  23107  finiunmbl  23119  volfiniun  23122  voliunlem3  23127  ioorinv  23150  ioorcl  23151  dyadmax  23172  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  volcn  23180  vitalilem2  23184  vitalilem3  23185  vitali  23188  i1fd  23254  itg2seq  23315  itg2addlem  23331  itgfsum  23399  ellimc3  23449  dvbsss  23472  dvnres  23500  dvmptfsum  23542  dvferm1lem  23551  dvferm2lem  23553  rolle  23557  c1lip1  23564  lhop1lem  23580  lhop1  23581  dvfsumlem2  23594  dvfsumlem4  23596  dvfsumrlim  23598  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  ftc1lem6  23608  mdegleb  23628  mdeglt  23629  deg1leb  23659  deg1lt  23661  ply1divex  23700  fta1glem2  23730  fta1g  23731  plyco0  23752  plyeq0lem  23770  coeeq2  23802  dgrle  23803  dgrcolem2  23834  dgrco  23835  plydivlem4  23855  plydivex  23856  fta1lem  23866  fta1  23867  vieta1lem2  23870  vieta1  23871  aalioulem2  23892  aalioulem4  23894  abelth  23999  cxpcn3  24289  rlimcnp  24492  xrlimcnp  24495  cxploglim  24504  scvxcvx  24512  jensen  24515  lgamgulmlem2  24556  wilthlem2  24595  wilthlem3  24596  fta  24606  dvdsmulf1o  24720  perfectlem2  24755  dchrelbas3  24763  dchrelbas4  24768  dchrn0  24775  bcmono  24802  lgsdir2lem4  24853  lgsdchr  24880  gausslemma2dlem0i  24889  lgseisenlem2  24901  lgsquad2lem2  24910  2sqlem6  24948  2sqlem8  24951  2sqlem10  24953  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  istrkgb  25154  istrkgcb  25155  istrkge  25156  axtgcgrid  25162  axtg5seg  25164  axtgbtwnid  25165  axtgpasch  25166  axtgcont1  25167  axtgeucl  25171  iscgrglt  25209  tgcgr4  25226  axcgrtr  25595  gropd  25708  grstructd  25709  upgredg2vtx  25814  upgredgpr  25815  wlkntrllem3  26091  1pthoncl  26122  2pthoncl  26133  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  fargshiftf1  26165  constr3trllem2  26179  clwwnisshclwwn  26337  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  eupatrl  26495  eupath2  26507  frgra3vlem1  26527  3vfriswmgralem  26531  3vfriswmgra  26532  frgrawopreglem4  26574  frg2wot1  26584  frg2woteqm  26586  usg2spot2nb  26592  numclwlk2lem2f1o  26632  friendshipgt3  26648  nvz  26908  nmobndseqi  27018  nmobndseqiALT  27019  nmlno0  27034  blocnilem  27043  dipdir  27081  dipass  27084  siilem2  27091  ubthlem2  27111  ubth  27113  htth  27159  normpyth  27386  norm3lemt  27393  chlimi  27475  chcompl  27483  omlsii  27646  pjoml  27679  h1de2i  27796  elspansn2  27810  h1datom  27825  pjoml2  27854  pjoml3  27855  lecm  27860  chscllem2  27881  osum  27888  spansncv  27896  pjcjt2  27935  pjopyth  27963  eigre  28078  eigorth  28081  hhcno  28147  hhcnf  28148  cnopc  28156  cnfnc  28173  nmcexi  28269  nmcopexi  28270  nmcfnexi  28294  pjssge0i  28409  hstel2  28462  stj  28478  stri  28500  hstri  28508  stcltr1i  28517  mdbr  28537  mdi  28538  mdbr3  28540  mdbr4  28541  dmdbr  28542  dmdmd  28543  dmdi  28545  dmdbr3  28548  dmdbr4  28549  dmdbr5  28551  mdsl1i  28564  mdslmd1lem3  28570  mdslmd1lem4  28571  mdslmd1i  28572  csmdsymi  28577  cvmd  28579  atss  28589  atom1d  28596  chcv1  28598  hatomic  28603  atord  28631  atcvat2  28632  mddmdin0i  28674  rmoxfrdOLD  28716  rmoxfrd  28717  ifeqeqx  28745  ssiun2sf  28760  ssrelf  28805  fmptcof2  28839  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1lem  28844  fz1nntr  28948  nn0min  28954  ressprs  28986  resspos  28990  toslublem  28998  tosglblem  29000  isomnd  29032  omndadd  29037  submarchi  29071  archirng  29073  archiexdiv  29075  archiabllem1a  29076  archiabllem2a  29079  archiabl  29083  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  xrge0tsmsd  29116  isorng  29130  orngmul  29134  isarchiofld  29148  fzto1st  29184  psgnfzto1st  29186  submateq  29203  lmatfval  29208  lmatcl  29210  iscref  29239  crefi  29242  pcmplfin  29255  xrge0iifiso  29309  esumcvg  29475  esum2dlem  29481  isrnsigaOLD  29502  sigaclcu  29507  sigaclci  29522  unelsiga  29524  unelldsys  29548  sigapildsys  29552  ldgenpisyslem1  29553  fiunelros  29564  measvun  29599  measiun  29608  carsgmon  29703  carsgsigalem  29704  carsgclctunlem2  29708  carsgclctun  29710  pmeasmono  29713  pmeasadd  29714  sibfof  29729  sitgclg  29731  eulerpartlemgvv  29765  signsply0  29954  signstfvneq0  29975  istrkg2d  29997  axtgupdim2OLD  29999  bnj1385  30157  bnj110  30182  bnj222  30207  bnj229  30208  bnj590  30234  bnj865  30247  bnj849  30249  bnj981  30274  bnj1014  30284  bnj1015  30285  bnj1112  30305  bnj1118  30306  bnj1123  30308  bnj1128  30312  bnj1125  30314  bnj1148  30318  bnj1154  30321  bnj1326  30348  bnj1384  30354  bnj1489  30378  bnj1497  30382  subfacp1lem6  30421  erdszelem9  30435  kur14lem9  30450  sconpht  30465  cvmsss2  30510  cvmliftlem7  30527  cvmliftlem10  30530  mclsrcl  30712  mclsssvlem  30713  mclsval  30714  mclsax  30720  mclsind  30721  mclsppslem  30734  iota5f  30861  dfpo2  30898  fununiq  30913  setinds  30927  dfon2lem3  30934  dfon2lem4  30935  dfon2lem5  30936  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon2  30941  tfisg  30960  frmin  30983  frinsg  30986  frrlem5e  31032  nocvxminlem  31089  btwnconn1lem11  31374  linethru  31430  fwddifnp1  31442  rankelg  31445  rankeq1o  31448  subtr  31478  subtr2  31479  trer  31480  nn0prpwlem  31487  nn0prpw  31488  neibastop2lem  31525  filnetlem4  31546  bj-hbxfrbi  31792  bj-nfbi  31793  bj-ssblem1  31819  bj-ssblem2  31820  bj-drnf1v  31938  bj-axext3  31957  bj-zfpow  31983  bj-nfbiit  32024  relowlssretop  32387  rdgeqoa  32394  finxpreclem6  32409  wl-mo3t  32537  wl-sb8mot  32539  finixpnum  32564  matunitlindflem1  32575  ptrest  32578  poimirlem13  32592  poimirlem14  32593  poimirlem17  32596  poimirlem18  32597  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem28  32607  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  poimir  32612  heicant  32614  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  voliunnfl  32623  volsupnfl  32624  mbfresfi  32626  itg2addnclem3  32633  itg2gt0cn  32635  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anclem7  32661  ftc1anc  32663  f1opr  32689  sdclem2  32708  fdc  32711  fdc1  32712  neificl  32719  mettrifi  32723  sstotbnd2  32743  cntotbnd  32765  heibor1lem  32778  bfp  32793  isass  32815  ismgmOLD  32819  isexid2  32824  iscringd  32967  ispridl  33003  pridl  33006  ismaxidl  33009  maxidlmax  33012  ispridlc  33039  pridlc  33040  dmnnzd  33044  axc11n-16  33241  ax12eq  33244  ax12el  33245  ax12inda  33251  ax12v2-o  33252  fsumshftd  33255  fsumshftdOLD  33256  riotasv2d  33261  lshpdisj  33292  lsmsatcv  33315  lsat0cv  33338  lcvexchlem4  33342  lcvexchlem5  33343  l1cvpat  33359  isopos  33485  oposlem  33487  isoml  33543  omllaw  33548  isatl  33604  atlex  33621  iscvlat  33628  cvlexch1  33633  glbconN  33681  hlsuprexch  33685  ps-1  33781  3atlem5  33791  psubspi  34051  llnexchb2  34173  elpcliN  34197  pclfinclN  34254  ldilval  34417  ltrnfset  34421  ltrnset  34422  ltrnu  34425  trlfset  34465  trlset  34466  trlval2  34468  cdleme25cv  34664  cdleme31so  34685  cdleme31fv  34696  cdlemefrs29bpre0  34702  cdleme32fva  34743  cdleme40v  34775  trlord  34875  cdlemkid3N  35239  cdlemkid4  35240  dihffval  35537  dihfval  35538  dihval  35539  lpolconN  35794  mapdordlem2  35944  hdmapfval  36137  hdmapval  36138  hdmapval2  36142  ismrcd1  36279  ismrcd2  36280  ismrc  36282  isnacs3  36291  nacsfix  36293  mzpcompact2  36333  fphpd  36398  fphpdo  36399  monotuz  36524  monotoddzzfi  36525  monotoddzz  36526  oddcomabszz  36527  zindbi  36529  setindtrs  36610  dford3lem2  36612  ttac  36621  dnnumch1  36632  fnwe2lem2  36639  aomclem3  36644  aomclem6  36647  aomclem8  36649  dfac11  36650  dfac21  36654  islssfg2  36659  hbtlem5  36717  hbt  36719  flcidc  36763  mendlmod  36782  sdrgacs  36790  ifpbi123  36854  rababg  36898  elmapintrab  36901  iunrelexpuztr  37030  frege92  37269  frege104  37281  ntrkbimka  37356  ntrk0kbimka  37357  neik0pk1imk0  37365  isotone1  37366  isotone2  37367  ntrclsiso  37385  ntrclskb  37387  ntrneiiso  37409  ntrneik3  37414  ntrneix3  37415  gneispacess2  37464  dvgrat  37533  cvgdvgrat  37534  binomcxplemnotnn0  37577  pm14.122b  37646  sbiota1  37657  sbcssOLD  37777  fnchoice  38211  fiiuncl  38259  iunincfi  38300  disjf1  38364  wessf1ornlem  38366  disjinfi  38375  axccdom  38411  dmrelrnrel  38414  axccd  38424  monoords  38452  fperiodmullem  38458  supxrgere  38490  supxrgelem  38494  supxrge  38495  xrlexaddrp  38509  infxr  38524  infleinf  38529  fsumclf  38633  fsumsplitf  38634  fsummulc1f  38635  fsumnncl  38638  fsumsplit1  38639  fsumf1of  38641  fsumreclf  38643  fsumlessf  38644  fsumsermpt  38646  fmul01  38647  fmulcl  38648  fmuldfeqlem1  38649  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  fprodexp  38661  fprodabs2  38662  fprodcnlem  38666  climmulf  38671  climexp  38672  climsuse  38675  climrecf  38676  climinff  38678  climaddf  38682  mullimc  38683  mullimcf  38690  idlimc  38693  limcperiod  38695  sumnnodd  38697  lptre2pt  38707  limsupre  38708  neglimc  38714  addlimc  38715  0ellimcdiv  38716  limclner  38718  climsubmpt  38727  climreclf  38731  climeldmeqmpt  38735  climfveqmpt  38738  fnlimfvre  38741  cncfshift  38759  cncfperiod  38764  icccncfext  38773  cncfiooicclem1  38779  fprodcncf  38787  fperdvper  38808  dvmptmulf  38827  dvnmptdivc  38828  dvnmul  38833  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  iblspltprt  38865  itgspltprt  38871  stoweidlem3  38896  stoweidlem4  38897  stoweidlem6  38899  stoweidlem8  38901  stoweidlem15  38908  stoweidlem16  38909  stoweidlem17  38910  stoweidlem19  38912  stoweidlem20  38913  stoweidlem22  38915  stoweidlem23  38916  stoweidlem26  38919  stoweidlem27  38920  stoweidlem30  38923  stoweidlem31  38924  stoweidlem32  38925  stoweidlem34  38927  stoweidlem35  38928  stoweidlem42  38935  stoweidlem43  38936  stoweidlem48  38941  stoweidlem50  38943  stoweidlem51  38944  stoweidlem57  38950  stoweidlem59  38952  stoweidlem62  38955  wallispilem3  38960  dirkercncflem2  38997  fourierdlem11  39011  fourierdlem12  39012  fourierdlem15  39015  fourierdlem16  39016  fourierdlem21  39021  fourierdlem34  39034  fourierdlem41  39041  fourierdlem42  39042  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem68  39067  fourierdlem71  39070  fourierdlem72  39071  fourierdlem73  39072  fourierdlem76  39075  fourierdlem79  39078  fourierdlem81  39080  fourierdlem83  39082  fourierdlem86  39085  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem94  39093  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  etransclem2  39129  etransclem46  39173  salunicl  39212  saluncl  39213  intsaluni  39223  dfsalgen2  39235  sge0f1o  39275  sge0lempt  39303  sge0iunmptlemfi  39306  sge0p1  39307  sge0fodjrnlem  39309  sge0iunmpt  39311  sge0ltfirpmpt2  39319  sge0isummpt2  39325  sge0xaddlem2  39327  sge0xadd  39328  nnfoctbdjlem  39348  meadjuni  39350  meadjiun  39359  voliunsge0lem  39365  meaiuninclem  39373  meaiininclem  39376  meaiininc  39377  omeunile  39395  isomenndlem  39420  ovn0lem  39455  ovnsubaddlem1  39460  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvle  39490  hspmbllem2  39517  hoimbl2  39555  vonhoire  39563  vonicclem2  39575  vonn0ioo2  39581  vonn0icc2  39583  salpreimagelt  39595  salpreimalegt  39597  pimdecfgtioc  39602  pimincfltioc  39603  pimincfltioo  39605  salpreimagtge  39611  salpreimaltle  39612  salpreimagtlt  39616  incsmf  39629  decsmf  39653  smflimlem1  39657  smflimlem2  39658  smflimlem3  39659  smflimlem4  39660  smonoord  39944  iccpartgt  39965  iccelpart  39971  iccpartiun  39972  icceuelpartlem  39973  icceuelpart  39974  iccpartnel  39976  fmtnofac2  40019  fmtnofac1  40020  prmdvdsfmtnof1lem2  40035  perfectALTVlem2  40165  bgoldbwt  40199  bgoldbst  40200  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  evengpop3  40214  evengpoap3  40215  bgoldbnnsum3prm  40220  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgblthelfgott  40229  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachOLD  40239  reuccatpfxs1lem  40296  fpropnf1  40337  usgredg2vtxeuALT  40449  nbgr2vtx1edg  40572  1wlkp1lem8  40889  upgrwlkdvdelem  40942  usgr2wlkneq  40962  usgr2pthlem  40969  pthdlem2lem  40973  uspgrn2crct  41011  2pthdlem1  41137  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  3pthdlem1  41331  eupth2  41407  frgr3vlem1  41443  3vfriswmgrlem  41447  frgrwopreglem4  41484  frgr2wwlk1  41494  frgr2wwlkeqm  41496  av-numclwlk2lem2f1o  41535  av-friendshipgt3  41552  ply1mulgsumlem2  41969  islininds  42029  linindslinci  42031  lindslinindsimp1  42040  linds0  42048  lindsrng01  42051  snlindsntorlem  42053  snlindsntor  42054  ldepsnlinc  42091  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213  nn0sumshdiglem2  42214  nn0sumshdig  42215  bnd2d  42226  setrec1lem1  42233  setrec1lem4  42236  setrec2fun  42238