Theorem imbi12d 345

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  imbi12  347  ifpbi123d  1084  nfbiit  1858  nfbidv  1929  sbjust  2072  nfbidf  2236  cbvsbvf  2371  drnf1v  2379  drnf1  2451  mo4  2570  cbvmovw  2606  cbvmow  2607  axextg  2713  rspw  3216  cbvralvw  3217  cbvralfw  3279  raleqbidv  3313  cbvraldva2  3315  sbralie  3317  sbralieOLD  3319  cbvralf  3324  ralcom2  3341  vtoclgaf  3519  vtoclga  3520  rspct  3546  rspc  3548  rspc2gv  3570  rexraleqim  3585  ralab2  3638  nelrdva  3646  mob2  3656  mob  3658  morex  3660  reu7  3673  reu8  3674  reu2eqd  3677  cdeqim  3714  sbcimg  3771  sbcim1  3776  sbceqal  3784  csbhypf  3859  cbvralcsf  3873  dfssf  3906  reldisj  4381  ralidmw  4444  reusngf  4606  rexreusng  4611  reuprg0  4634  elpreqpr  4798  unissb  4871  intss1  4893  intmin  4898  dftr2c  5182  trel  5187  zfpow  5295  reusv2lem4  5330  reusv3i  5333  rext  5387  opth  5416  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  poeq1  5529  pocl  5534  swopolem  5536  swopo  5537  isso2i  5563  vtoclr  5681  poinxp  5699  posn  5704  ssrel  5726  ssrel2  5728  ssrelrel  5739  relop  5792  cotrg  6061  cnvsym  6064  reu3op  6243  reuop  6244  dfpo2  6247  preddowncl  6283  frpoinsg  6294  ordelord  6332  iota5  6468  dffun2  6495  sbcfung  6509  funopg  6519  brprcneu  6817  brprcneuALT  6818  tz6.12f  6852  funbrfv  6875  ssimaexg  6913  fvmptf  6957  fvelrn  7017  fprg  7098  dff13f  7199  f1veqaeq  7200  fpropnf1  7211  f1ounsn  7216  nf1const  7248  soisores  7271  soisoi  7272  isofrlem  7284  isopolem  7289  weniso  7298  riota5f  7341  imbrov2fvoveq  7381  oprabidw  7387  oprabid  7388  f1opr  7412  ovmpos  7504  ov2gf  7505  ov3  7519  caovcan  7560  caovordig  7561  caofrss  7659  caoftrn  7661  tfisg  7794  tfis  7795  tfisi  7799  tfindsg  7801  tfindsg2  7802  tfindes  7803  dfom2  7808  limomss  7811  nnlim  7820  peano5  7833  findsg  7837  findes  7840  resf1extb  7874  f1oweALT  7914  dfoprab4f  7998  offval22  8027  f1o2ndf1  8061  frxp  8066  poxp  8068  frpoins3xpg  8080  frpoins3xp3g  8081  poxp2  8083  frxp2  8084  xpord2indlem  8087  poxp3  8090  frxp3  8091  xpord3inddlem  8094  suppfnss  8129  onfununi  8271  smoel  8290  smogt  8297  tfrlem1  8305  tz7.48lem  8370  tz7.49  8374  oawordeu  8480  omordi  8491  oeordi  8513  nnmordi  8557  omabs  8577  nneob  8582  omsmolem  8583  qsel  8733  eroveu  8749  ecopovtrn  8757  ixpsnf1o  8876  fundmeng  8969  sbth  9025  limensuc  9082  findcard  9088  findcard2  9089  findcard2d  9091  pssnn  9093  ssfi  9097  sbthfi  9123  nneneq  9130  php  9131  unxpdom  9159  findcard3  9183  ac6sfi  9184  frfi  9185  domunfican  9222  fiint  9227  iunfi  9243  finsschain  9259  dffi3  9334  marypha1lem  9336  marypha1  9337  supeq3  9352  supeq123d  9353  supmo  9355  suplub  9363  supisolem  9377  eqinf  9388  infval  9390  infmo  9400  ordiso2  9420  ordtypelem7  9429  wemaplem1  9451  wemaplem2  9452  zfregcl  9499  zfregclOLD  9500  elirrv  9502  elirrvOLD  9503  inf0  9533  inf3lem1  9540  zfinf  9551  axinf2  9552  dfom3  9559  elom3  9560  cantnfval2  9581  cantnfle  9583  cantnflt  9584  cantnfp1lem3  9592  oemapvali  9596  cantnflem1c  9599  cantnflem1  9601  cantnf  9605  wemapwe  9609  cnfcom  9612  ttrclss  9632  ttrclselem2  9638  setind  9659  setinds  9661  frmin  9664  frinsg  9666  r1sdom  9689  r1ordg  9693  rankonidlem  9743  rankunb  9765  bnd2  9808  infxpenlem  9926  infxpenc2  9935  dfac8alem  9942  dfac8clem  9945  indcardi  9954  alephordi  9987  alephinit  10008  alephfp  10021  aceq3lem  10033  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  dfac9  10050  dfac12lem2  10058  dfac12lem3  10059  kmlem1  10064  kmlem4  10067  kmlem10  10073  kmlem12  10075  kmlem13  10076  pwsdompw  10116  ackbij1lem16  10147  cfslb2n  10181  cfsmolem  10183  sornom  10190  fin2i  10208  infpssrlem4  10219  isfin2-2  10232  isfin3ds  10242  fin23lem17  10251  fin23lem32  10257  fin23lem34  10259  fin23lem35  10260  fin23lem39  10263  fin23lem41  10265  isf32lem2  10267  isf33lem  10279  isf34lem4  10290  isf34lem6  10293  fin1a2lem10  10322  axcc2lem  10349  axcc3  10351  axcc4dom  10354  dominf  10358  axdc2lem  10361  axdc3lem2  10364  ac6sg  10401  zorn2lem7  10415  zornn0g  10418  ttukeylem5  10426  ttukeylem6  10427  axdclem  10432  dominfac  10487  axrepndlem1  10506  axrepndlem2  10507  axunndlem1  10509  axunnd  10510  axpowndlem2  10512  axpowndlem3  10513  axpowndlem4  10514  axregndlem2  10517  axregnd  10518  axinfndlem1  10519  axinfnd  10520  axacndlem4  10524  axacndlem5  10525  axacnd  10526  zfcndpow  10530  zfcndinf  10532  fpwwe2lem4  10548  fpwwe2lem7  10551  fpwwe2lem11  10555  pwfseqlem4a  10575  pwfseqlem4  10576  pwfseqlem5  10577  pwfseq  10578  wunfi  10635  wunex2  10652  inar1  10689  rankcf  10691  tskord  10694  grudomon  10731  grur1a  10733  axgroth6  10742  axgroth3  10745  axgroth4  10746  eltskm  10757  indpi  10821  pinq  10841  nqereu  10843  prcdnq  10907  prnmax  10909  ltsopr  10946  prlem936  10961  ltsosr  11008  recexsrlem  11017  mulgt0sr  11019  map2psrpr  11024  supsrlem  11025  axrrecex  11077  axpre-lttrn  11080  axpre-mulgt0  11082  axpre-sup  11083  axsup  11212  dedekind  11300  ltordlem  11666  ltord1  11667  wloglei  11673  squeeze0  12050  infm3  12106  nnsub  12212  nnunb  12424  peano5uzti  12610  fzind  12618  uzind4s  12849  uzind4s2  12850  zmax  12886  zbtwnre  12887  xmulasslem  13228  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  infmremnf  13287  injresinj  13737  om2uzlti  13903  uzindi  13935  axdc4uz  13937  ssnn0fi  13938  rabssnn0fi  13939  suppssfz  13947  seqp1  13969  seqcl2  13973  seqfveq2  13977  seqshft2  13981  monoord  13985  seqsplit  13988  seqf1olem2  13995  seqf1o  13996  seqid2  14001  seqhomo  14002  seqof2  14013  expcl2lem  14026  facdiv  14240  facwordi  14242  faclbnd4lem2  14247  hashnn0n0nn  14344  hashf1lem2  14409  seqcoll  14417  fi1uzind  14460  brfi1indALT  14463  wrdind  14675  wrd2ind  14676  swrdccatin1  14678  swrdccat3blem  14692  reuccatpfxs1lem  14699  repswccat  14739  cshf1  14763  trclfvcotr  14962  relexprelg  14991  rtrclreclem4  15014  relexpindlem  15016  ello1mpt  15474  o1co  15539  o1compt  15540  rlimcn3  15543  climcn2  15546  subcn2  15548  o1of2  15566  fsumclf  15691  fsumsplitf  15695  fsumsplit1  15698  fsum2d  15724  modfsummod  15748  fsumabs  15755  telfsumo  15756  fsumrlim  15765  fsumo1  15766  o1fsum  15767  fsumiun  15775  prodfdiv  15852  fprod2d  15937  fproddivf  15943  fprodsplitf  15944  fprodsplit1f  15946  rpnnen2lem10  16181  sqrt2irr  16207  dvdsle  16270  divalglem7  16359  divalglem8  16360  ndvdssub  16369  gcdcllem1  16459  dfgcd2  16506  algcvg  16536  algcvga  16539  algfx  16540  lcmgcdlem  16566  lcmdvds  16568  lcmf  16593  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem  16601  lcmfdvds  16602  lcmfun  16605  coprmgcdb  16609  coprmdvds1  16612  coprmdvds2  16614  coprmprod  16621  coprmproddvds  16623  prmind2  16645  dvdsprime  16647  nprm  16648  dvdsprm  16664  exprmfct  16665  coprm  16672  isprm6  16675  prmfac1  16681  eulerthlem2  16743  pcqmul  16815  pcqcl  16818  pc2dvds  16841  pcz  16843  prmpwdvds  16866  infpn2  16875  vdwlem12  16954  ramub2  16976  rami  16977  ramcl  16991  prmdvdsprmop  17005  prmlem0  17067  mreintcl  17548  ismred2  17556  mrissmrcd  17597  mreexexlemd  17601  iscatd2  17638  moni  17694  yoniso  18242  isprs  18253  prslem  18254  drsdirfi  18262  ispos  18271  posi  18274  isposd  18279  pospropd  18282  lubfval  18305  lublecllem  18315  glbfval  18318  joinle  18341  meetle  18355  poslubmo  18366  posglbmo  18367  resspos  18386  lubl  18469  lubun  18472  clatleglb  18475  ipodrsima  18498  acsdrsel  18500  isacs4lem  18501  isacs5lem  18502  acsdrscl  18503  mreclatBAD  18520  pslem  18529  dirtr  18559  chnind  18578  mndind  18787  mhmlem  19029  isnsg2  19122  ghmf1  19212  orbsta  19279  symgextf1  19387  gsmsymgrfix  19394  gsmsymgreq  19398  symggen  19436  psgnunilem4  19463  sylow1lem1  19564  sylow2alem2  19584  sylow2a  19585  lsmmod  19641  lsmdisj2  19648  efgsrel  19700  efgredlemd  19710  efgredlem  19713  efgred  19714  gsumzaddlem  19887  gsummptnn0fz  19952  gsummptnn0fzfv  19953  telgsumfzs  19955  telgsums  19959  dprdval  19971  dprddisj2  20007  ablfac1eulem  20040  pgpfac1lem1  20042  pgpfac1lem5  20047  pgpfac1  20048  pgpfaclem2  20050  pgpfac  20052  isomnd  20089  omndadd  20094  gsumle  20111  irredmul  20400  islring  20512  lringuplu  20516  rrgval  20669  rrgeq0i  20671  isdomn  20677  domneq0  20680  isdomn4  20688  domnlcanb  20692  domnrcanb  20694  isdrngrd  20738  isdrngrdOLD  20740  sdrgacs  20773  isorng  20833  orngmul  20837  islbs3  21148  rngqiprngimf1lem  21287  cnsubrglem  21392  prmirredlem  21447  znfld  21535  znrrg  21540  cygznlem3  21544  isphl  21603  ipeq0  21613  isphld  21629  phlpropd  21630  lsmcss  21667  frlmphl  21756  frlmup1  21773  lindfrn  21796  islindf4  21813  islindf5  21814  mplsubglem  21973  mpllsslem  21974  mplcoe1  22013  mplcoe5  22016  mpfind  22091  ismhp3  22130  coe1fzgsumd  22290  gsummoncoe1  22294  pf1ind  22341  evl1gsumd  22343  dmatelnd  22479  mat1scmat  22522  mdetdiaglem  22581  mdetralt  22591  mdetralt2  22592  mdetunilem1  22595  mdetunilem2  22596  mdetunilem3  22597  mdetunilem4  22598  mdetunilem9  22603  smadiadetr  22658  pmatcoe1fsupp  22684  mp2pm2mplem4  22792  uniopn  22880  fiinopn  22884  epttop  22992  clsndisj  23058  elcls3  23066  neiptoptop  23114  neiptopnei  23115  cnpval  23219  iscnp  23220  cnpimaex  23239  lmcvg  23245  cnprest  23272  cnprest2  23273  lmss  23281  lmff  23284  t0sep  23307  hausnei  23311  isnrm2  23341  t1sep2  23352  isreg2  23360  iscmp  23371  cmpcov  23372  cmpsublem  23382  cmpsub  23383  tgcmp  23384  uncmp  23386  fiuncmp  23387  hauscmplem  23389  cmpfi  23391  cmpfii  23392  dfconn2  23402  connsuba  23403  connsub  23404  nconnsubb  23406  1stcclb  23427  1stcfb  23428  2ndc1stc  23434  1stcrest  23436  1stcelcls  23444  restnlly  23465  lly1stc  23479  comppfsc  23515  kgenval  23518  kgeni  23520  kgencn2  23540  ptcldmpt  23597  ptclsg  23598  dfac14lem  23600  dfac14  23601  txcnp  23603  ptcnp  23605  hausdiag  23628  txlm  23631  tx1stc  23633  xkococn  23643  cnmpt12  23650  cnmpt22  23657  kqt0lem  23719  isr0  23720  regr1lem2  23723  kqreglem1  23724  r0sep  23731  ptcmpfi  23796  elmptrab  23810  isfil  23830  filss  23836  isufil2  23891  cfinufil  23911  rnelfm  23936  fmfnfmlem2  23938  fmfnfmlem4  23940  flimopn  23958  flimrest  23966  flftg  23979  cnpflf  23984  txflf  23989  fclsopni  23998  fclsrest  24007  fclscf  24008  flimfnfcls  24011  fcfnei  24018  alexsublem  24027  alexsubb  24029  alexsubALTlem3  24032  alexsubALTlem4  24033  alexsubALT  24034  cnextcn  24050  cnextfres1  24051  tgpt0  24102  qustgplem  24104  tsmsi  24117  tsmssubm  24126  tsmsres  24127  tsmsf1o  24128  tsmsxp  24138  ustssel  24189  ust0  24203  ustuqtop4  24227  ucnima  24263  ucncn  24267  iscusp  24281  cuspcvg  24283  imasdsf1olem  24356  blssps  24407  blss  24408  metss  24491  comet  24496  metcnp3  24523  metcnp2  24525  txmetcnp  24530  metuel2  24548  metucn  24554  nrmmetd  24557  nlmvscn  24670  nrginvrcn  24675  nmolb  24700  xrge0tsms  24818  mpomulcn  24852  divcn  24853  fsumcn  24855  elcncf2  24875  cncfi  24879  mulc1cncf  24890  cncfmet  24894  xrhmeo  24931  bndth  24943  nmoleub2lem2  25101  nmoleub3  25104  ipcn  25231  lmmbr  25243  caucfil  25268  pmltpc  25435  ovolfiniun  25486  ovolicc2lem3  25504  ovolicc2  25507  mblsplit  25517  finiunmbl  25529  volfiniun  25532  voliunlem3  25537  ioorinv  25561  ioorcl  25562  dyadmax  25583  dyadmbllem  25584  dyadmbl  25585  opnmbllem  25586  volcn  25591  vitalilem2  25594  vitalilem3  25595  vitali  25598  i1fd  25666  itg2seq  25727  itg2addlem  25743  itgfsum  25812  ellimc3  25864  dvbsss  25887  dvnres  25916  dvmptfsum  25960  dvferm1lem  25969  dvferm2lem  25971  rolle  25975  c1lip1  25982  lhop1lem  25998  lhop1  25999  dvfsumlem2  26012  dvfsumlem4  26014  dvfsumrlim  26016  dvfsum2  26019  ftc1a  26022  ftc1lem6  26026  mdegleb  26047  mdeglt  26048  deg1leb  26078  deg1lt  26080  ply1divex  26120  fta1glem2  26152  fta1g  26153  plyco0  26175  plyeq0lem  26193  coeeq2  26225  dgrle  26226  dgrcolem2  26257  dgrco  26258  plydivlem4  26280  plydivex  26281  fta1lem  26291  fta1  26292  vieta1lem2  26295  vieta1  26296  aalioulem2  26317  aalioulem4  26319  abelth  26424  cxpcn3  26730  rlimcnp  26947  xrlimcnp  26950  cxploglim  26959  scvxcvx  26967  jensen  26970  lgamgulmlem2  27011  wilthlem2  27050  wilthlem3  27051  fta  27061  mpodvdsmulf1o  27175  dvdsmulf1o  27177  perfectlem2  27211  dchrelbas3  27219  dchrelbas4  27224  dchrn0  27231  bcmono  27258  lgsdir2lem4  27309  lgsdchr  27336  gausslemma2dlem0i  27345  lgseisenlem2  27357  lgsquad2lem2  27366  2sqlem6  27404  2sqlem8  27407  2sqlem10  27409  dchrisumlema  27469  dchrisumlem2  27471  dchrisumlem3  27472  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem3  27692  nosupbnd1lem5  27694  nosupbnd2  27698  noinfcbv  27699  noinfdm  27701  noinffv  27703  noinfres  27704  noinfbnd1lem1  27705  noinfbnd1lem3  27707  noinfbnd1lem5  27709  noinfbnd2  27713  nocvxminlem  27764  madebdaylemold  27908  madebdaylemlrcut  27909  madebday  27910  lrrecpo  27951  addsproplem1  27979  addsprop  27986  leadds1  27999  negsproplem1  28038  negsprop  28045  mulsproplemcbv  28125  mulsproplem1  28126  mulsprop  28140  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  precsex  28228  bdayons  28286  addonbday  28289  onsfi  28366  n0subs  28373  oldfib  28387  eln0zs  28410  bdaypw2n0bndlem  28473  bdaypw2n0bnd  28474  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  bdayfinbnd  28479  istrkgb  28541  istrkgcb  28542  istrkge  28543  axtgcgrid  28549  axtg5seg  28551  axtgbtwnid  28552  axtgpasch  28553  axtgcont1  28554  axtgeucl  28558  iscgrglt  28600  tgcgr4  28617  axcgrtr  29002  gropd  29118  grstructd  29119  upgredg2vtx  29228  upgredgpr  29229  edglnl  29230  numedglnl  29231  usgredg2vtxeuALT  29309  nbgr2vtx1edg  29437  finsumvtxdg2size  29637  wlkp1lem8  29765  upgrwlkdvdelem  29822  usgr2wlkneq  29842  usgr2pthlem  29849  pthdlem2lem  29853  uspgrn2crct  29894  2pthdlem1  30016  eleclclwwlkn  30164  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  3pthdlem1  30252  eupth2  30327  frgr3vlem1  30361  3vfriswmgrlem  30365  frgrwopreglem4a  30398  frgr2wwlk1  30417  wlkl0  30455  numclwlk2lem2f1o  30467  friendshipgt3  30486  eulplig  30574  nvz  30758  nmobndseqi  30868  nmobndseqiALT  30869  nmlno0  30884  blocnilem  30893  dipdir  30931  dipass  30934  siilem2  30941  ubthlem2  30960  ubth  30962  htth  31007  normpyth  31234  norm3lemt  31241  chlimi  31323  chcompl  31331  omlsii  31492  pjoml  31525  h1de2i  31642  elspansn2  31656  h1datom  31671  pjoml2  31700  pjoml3  31701  lecm  31706  chscllem2  31727  osum  31734  spansncv  31742  pjcjt2  31781  pjopyth  31809  eigre  31924  eigorth  31927  hhcno  31993  hhcnf  31994  cnopc  32002  cnfnc  32019  nmcexi  32115  nmcopexi  32116  nmcfnexi  32140  pjssge0i  32255  hstel2  32308  stj  32324  stri  32346  hstri  32354  stcltr1i  32363  mdbr  32383  mdi  32384  mdbr3  32386  mdbr4  32387  dmdbr  32388  dmdmd  32389  dmdi  32391  dmdbr3  32394  dmdbr4  32395  dmdbr5  32397  mdsl1i  32410  mdslmd1lem3  32416  mdslmd1lem4  32417  mdslmd1i  32418  csmdsymi  32423  cvmd  32425  atss  32435  atom1d  32442  chcv1  32444  hatomic  32449  atord  32477  atcvat2  32478  mddmdin0i  32520  opreu2reuALT  32564  rmoxfrd  32580  ifeqeqx  32630  ssiun2sf  32648  iinabrex  32658  ssrelf  32707  fmptcof2  32749  acunirnmpt  32751  acunirnmpt2  32752  acunirnmpt2f  32753  aciunf1lem  32754  suppovss  32773  fz1nntr  32894  nn0min  32913  fsumiunle  32921  wrdt2ind  33032  ressprs  33045  toslublem  33051  tosglblem  33053  mntoval  33061  ismntd  33063  dfmgc2lem  33074  dfmgc2  33075  xrge0tsmsd  33154  fzto1st  33184  psgnfzto1st  33186  submarchi  33267  archirng  33269  archiexdiv  33271  archiabllem1a  33272  archiabllem2a  33275  archiabl  33279  isarchiofld  33280  gsumvsca1  33307  gsumvsca2  33308  elrgspnlem4  33326  domnpropd  33358  domnlcanOLD  33361  linds2eq  33464  isprmidl  33521  prmidl  33523  prmidlc  33531  ssdifidlprm  33541  ismxidl  33545  mxidlmax  33548  rprmval  33599  isrprm  33600  rprmdvds  33602  rprmdvdsprod  33617  1arithidomlem1  33618  1arithidom  33620  1arithufdlem3  33629  dfufd2lem  33632  lbsdiflsp0  33810  fedgmullem1  33813  fedgmullem2  33814  fldext2chn  33912  constrmon  33928  submateq  33993  lmatfval  33998  lmatcl  34000  iscref  34028  crefi  34031  pcmplfin  34044  xrge0iifiso  34119  esumcvg  34270  esum2dlem  34276  sigaclcu  34301  sigaclci  34316  unelsiga  34318  unelldsys  34342  sigapildsys  34346  ldgenpisyslem1  34347  fiunelros  34358  measvun  34393  measiun  34402  carsgmon  34498  carsgsigalem  34499  carsgclctunlem2  34503  carsgclctun  34505  pmeasmono  34508  pmeasadd  34509  sibfof  34524  sitgclg  34526  eulerpartlemgvv  34560  signsply0  34735  signstfvneq0  34756  breprexp  34817  hgt749d  34833  istrkg2d  34850  axtgupdim2ALTV  34852  bnj1385  35014  bnj110  35040  bnj222  35065  bnj229  35066  bnj590  35092  bnj865  35105  bnj849  35107  bnj981  35132  bnj1014  35143  bnj1015  35144  bnj1112  35165  bnj1118  35166  bnj1123  35168  bnj1128  35172  bnj1125  35174  bnj1148  35178  bnj1154  35181  bnj1326  35208  bnj1384  35214  bnj1489  35238  bnj1497  35242  funen1cnv  35269  r1filimi  35284  trssfir1om  35292  r1omhfb  35293  setindregs  35311  trssfir1omregs  35317  r1omhfbregs  35318  axpowg  35327  onvf1odlem2  35332  f1resfz0f1d  35342  cplgredgex  35349  acycgrcycl  35375  subfacp1lem6  35413  erdszelem9  35427  kur14lem9  35442  sconnpht  35457  cvmsss2  35502  cvmliftlem7  35519  cvmliftlem10  35522  fmlasuc  35614  gonar  35623  goalr  35625  mclsrcl  35789  mclsssvlem  35790  mclsval  35791  mclsax  35797  mclsind  35798  mclsppslem  35811  iota5f  35952  fununiq  35997  dfon2lem3  36011  dfon2lem4  36012  dfon2lem5  36013  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  dfon2  36018  btwnconn1lem11  36325  linethru  36381  fwddifnp1  36393  rankelg  36396  rankeq1o  36399  sbequbidv  36442  cbvralvw2  36454  cbvmodavw  36478  cbvsbdavw  36482  cbvsbdavw2  36483  subtr  36542  subtr2  36543  trer  36544  nn0prpwlem  36550  nn0prpw  36551  neibastop2lem  36588  filnetlem4  36609  axtco1from2  36703  axtcond  36706  axuntco  36707  dfttc4lem2  36757  dfttc4  36758  mh-setindnd  36765  regsfromregtco  36766  regsfromsetind  36767  mh-inf3f1  36769  mh-unprimbi  36772  mh-infprim2bi  36775  bj-hbxfrbi  36953  bj-hbyfrbi  36954  bj-ssblem1  36994  bj-ssblem2  36995  bj-ax12  36997  irrdiff  37686  relowlssretop  37725  rdgeqoa  37732  rdgssun  37740  exrecfnlem  37741  finxpreclem6  37758  pibp19  37776  pibt2  37779  wl-ax12v2cl  37868  wl-mo3t  37947  wl-sb8mot  37951  wl-sb8motv  37952  finixpnum  37972  matunitlindflem1  37983  ptrest  37986  poimirlem13  38000  poimirlem14  38001  poimirlem17  38004  poimirlem18  38005  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  poimirlem28  38015  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  poimir  38020  heicant  38022  mblfinlem1  38024  mblfinlem2  38025  mblfinlem3  38026  voliunnfl  38031  volsupnfl  38032  mbfresfi  38033  itg2addnclem3  38040  ftc1cnnc  38059  ftc1anclem7  38066  ftc1anc  38068  sdclem2  38109  fdc  38112  fdc1  38113  neificl  38120  mettrifi  38124  sstotbnd2  38141  cntotbnd  38163  heibor1lem  38176  bfp  38191  isass  38213  ismgmOLD  38217  isexid2  38222  iscringd  38365  ispridl  38401  pridl  38404  ismaxidl  38407  maxidlmax  38410  ispridlc  38437  pridlc  38438  dmnnzd  38442  relcnveq2  38696  ecin0  38719  elrelscnveq2  38996  elsymrels3  39005  eltrrels3  39031  eleqvrels3  39044  eqvrelqsel  39067  disjimeceqim2  39172  eldisjim3  39182  eldisjlem19  39280  eldisjsim3  39304  axc11n-16  39430  ax12eq  39433  ax12el  39434  ax12inda  39440  ax12v2-o  39441  fsumshftd  39444  riotasv2d  39449  lshpdisj  39479  lsmsatcv  39502  lsat0cv  39525  lcvexchlem4  39529  lcvexchlem5  39530  l1cvpat  39546  isopos  39672  oposlem  39674  isoml  39730  omllaw  39735  isatl  39791  atlex  39808  iscvlat  39815  cvlexch1  39820  glbconN  39869  hlsuprexch  39873  ps-1  39969  3atlem5  39979  psubspi  40239  llnexchb2  40361  elpcliN  40385  pclfinclN  40442  ldilval  40605  ltrnfset  40609  ltrnset  40610  ltrnu  40613  trlfset  40652  trlset  40653  trlval2  40655  cdleme25cv  40850  cdleme31so  40871  cdleme31fv  40882  cdlemefrs29bpre0  40888  cdleme32fva  40929  cdleme40v  40961  trlord  41061  cdlemkid3N  41425  cdlemkid4  41426  dihffval  41722  dihfval  41723  dihval  41724  lpolconN  41979  mapdordlem2  42129  hdmapfval  42319  hdmapval  42320  hdmapval2  42324  aks4d1p7  42568  isprimroot  42578  primrootlekpowne0  42590  sticksstones1  42631  sticksstones2  42632  sticksstones10  42640  sticksstones12a  42642  aks6d1c6lem3  42657  indstrd  42678  unitscyglem2  42681  unitscyglem3  42682  unitscyglem4  42683  nnn1suc  42749  fsuppind  43040  eu6w  43126  ismrcd1  43147  ismrcd2  43148  ismrc  43150  isnacs3  43159  nacsfix  43161  mzpcompact2  43201  fphpd  43261  fphpdo  43262  monotuz  43386  monotoddzzfi  43387  monotoddzz  43388  oddcomabszz  43389  zindbi  43391  setindtrs  43470  dford3lem2  43472  ttac  43481  dnnumch1  43489  fnwe2lem2  43496  aomclem3  43501  aomclem6  43504  aomclem8  43506  dfac11  43507  dfac21  43511  islssfg2  43516  hbtlem5  43573  hbt  43575  flcidc  43615  mendlmod  43634  unielss  43663  rababg  44018  elmapintrab  44020  iunrelexpuztr  44163  frege92  44399  frege104  44411  ntrkbimka  44482  ntrk0kbimka  44483  neik0pk1imk0  44491  isotone1  44492  isotone2  44493  ntrclsiso  44511  ntrclskb  44513  ntrneiiso  44535  ntrneik3  44540  ntrneix3  44541  gneispacess2  44590  grur1cld  44676  scottabf  44684  ismnu  44705  mnuop23d  44710  mnuunid  44721  ismnushort  44745  dvgrat  44756  cvgdvgrat  44757  binomcxplemnotnn0  44800  pm14.122b  44867  sbiota1  44878  relprel  45395  relpfrlem  45397  modelaxreplem1  45422  modelaxreplem2  45423  modelaxrep  45425  omssaxinf2  45432  modelac8prim  45436  permaxinf2lem  45456  permac8prim  45458  nregmodel  45461  fnchoice  45477  fiiuncl  45513  iunincfi  45541  disjf1  45630  wessf1ornlem  45632  disjinfi  45639  axccdom  45667  dmrelrnrel  45671  axccd  45673  monoords  45745  fperiodmullem  45751  supxrgere  45778  supxrgelem  45782  supxrge  45783  xrlexaddrp  45797  infxr  45811  infleinf  45816  supxrleubrnmptf  45894  monoordxrv  45924  monoordxr  45925  monoord2xr  45927  fsummulc1f  46016  fsumnncl  46017  fsumf1of  46019  fsumreclf  46021  fsumlessf  46022  fsumsermpt  46024  fmul01  46025  fmulcl  46026  fmuldfeqlem1  46027  fmuldfeq  46028  fmul01lt1lem1  46029  fmul01lt1lem2  46030  fprodexp  46039  fprodabs2  46040  fprodcnlem  46044  climmulf  46049  climexp  46050  climsuse  46053  climrecf  46054  climinff  46056  climaddf  46060  mullimc  46061  mullimcf  46068  limcperiod  46073  sumnnodd  46075  lptre2pt  46083  limsupre  46084  neglimc  46090  addlimc  46091  0ellimcdiv  46092  limclner  46094  climsubmpt  46103  climreclf  46107  climeldmeqmpt  46111  climfveqmpt  46114  fnlimfvre  46117  climfveqf  46123  climfveqmpt3  46125  climeldmeqf  46126  limsupref  46128  limsupbnd1f  46129  climeqf  46131  climeldmeqmpt3  46132  climinf2  46150  limsupubuz  46156  climinf2mpt  46157  climinfmpt  46158  limsupmnf  46164  limsupequz  46166  limsupre2  46168  limsupequzmptf  46174  limsupre3  46176  lmbr3  46190  cnrefiisp  46273  xlimxrre  46274  xlimmnfvlem1  46275  xlimpnfvlem1  46279  climxlim2lem  46288  cncfshift  46317  cncfperiod  46322  icccncfext  46330  fprodcncf  46343  fperdvper  46362  dvmptmulf  46380  dvnmptdivc  46381  dvnmul  46386  dvmptfprod  46388  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  iblspltprt  46416  itgspltprt  46422  stoweidlem3  46446  stoweidlem4  46447  stoweidlem6  46449  stoweidlem8  46451  stoweidlem15  46458  stoweidlem16  46459  stoweidlem17  46460  stoweidlem19  46462  stoweidlem20  46463  stoweidlem22  46465  stoweidlem23  46466  stoweidlem26  46469  stoweidlem27  46470  stoweidlem30  46473  stoweidlem31  46474  stoweidlem32  46475  stoweidlem34  46477  stoweidlem35  46478  stoweidlem42  46485  stoweidlem43  46486  stoweidlem48  46491  stoweidlem50  46493  stoweidlem51  46494  stoweidlem57  46500  stoweidlem59  46502  stoweidlem62  46505  wallispilem3  46510  dirkercncflem2  46547  fourierdlem11  46561  fourierdlem12  46562  fourierdlem15  46565  fourierdlem16  46566  fourierdlem21  46571  fourierdlem34  46584  fourierdlem41  46591  fourierdlem42  46592  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem51  46600  fourierdlem68  46617  fourierdlem71  46620  fourierdlem72  46621  fourierdlem73  46622  fourierdlem76  46625  fourierdlem79  46628  fourierdlem81  46630  fourierdlem83  46632  fourierdlem86  46635  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem92  46641  fourierdlem94  46643  fourierdlem97  46646  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  etransclem2  46679  etransclem46  46723  salunicl  46759  saluncl  46760  intsaluni  46772  dfsalgen2  46784  sge0f1o  46825  sge0lempt  46853  sge0iunmptlemfi  46856  sge0p1  46857  sge0fodjrnlem  46859  sge0iunmpt  46861  sge0ltfirpmpt2  46869  sge0isummpt2  46875  sge0xaddlem2  46877  sge0xadd  46878  nnfoctbdjlem  46898  meadjuni  46900  meadjiun  46909  voliunsge0lem  46915  meaiuninclem  46923  meaiunincf  46926  meaiuninc3v  46927  meaiuninc3  46928  meaiininclem  46929  meaiininc  46930  omeunile  46948  isomenndlem  46973  ovn0lem  47008  ovnsubaddlem1  47013  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvle  47043  hspmbllem2  47070  hoimbl2  47108  vonhoire  47115  vonicclem2  47127  vonn0ioo2  47133  vonn0icc2  47135  salpreimagelt  47150  salpreimalegt  47152  pimdecfgtioc  47158  pimincfltioc  47159  pimincfltioo  47161  salpreimagtge  47168  salpreimaltle  47169  salpreimagtlt  47173  incsmf  47185  decsmf  47210  smflimlem1  47214  smflimlem2  47215  smflimlem3  47216  smflimlem4  47217  smfpimcclem  47250  funressnmo  47509  fcoresf1  47532  aiota0def  47559  euoreqb  47572  2reu8i  47576  2reuimp0  47577  funressndmafv2rn  47686  funressnbrafv2  47707  funbrafv2  47710  smonoord  47840  elsetpreimafvbi  47866  iccpartgt  47902  iccelpart  47908  iccpartiun  47909  icceuelpartlem  47910  icceuelpart  47911  iccpartnel  47913  fargshiftf1  47916  ichexmpl2  47945  ichnreuop  47947  ichreuopeq  47948  sprsymrelfolem2  47968  prproropf1olem4  47981  paireqne  47986  reupr  47997  reuopreuprim  48001  fmtnofac2  48047  fmtnofac1  48048  prmdvdsfmtnof1lem2  48063  perfectALTVlem2  48213  nfermltl8rev  48233  nfermltl2rev  48234  sbgoldbwt  48268  sbgoldbst  48269  sgoldbeven3prm  48274  sbgoldbm  48275  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  evengpop3  48289  evengpoap3  48290  bgoldbnnsum3prm  48295  bgoldbtbndlem4  48299  bgoldbtbnd  48300  tgblthelfgott  48306  tgoldbach  48308  grimuhgr  48378  grimcnv  48379  isuspgrimlem  48386  isubgr3stgrlem4  48460  isubgr3stgrlem6  48462  isubgr3stgrlem7  48463  gpgedg2ov  48557  gpgedg2iv  48558  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  pgnbgreunbgr  48616  ply1mulgsumlem2  48878  islininds  48937  linindslinci  48939  lindslinindsimp1  48948  linds0  48956  lindsrng01  48959  snlindsntorlem  48961  snlindsntor  48962  ldepsnlinc  48999  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  nn0sumshdiglem2  49113  nn0sumshdig  49114  itschlc0yqe  49251  f1mo  49343  iscnrm3lem5  49427  iscnrm3r  49438  isprsd  49445  lubeldm2d  49448  glbeldm2d  49449  joindm2  49458  meetdm2  49460  ipolublem  49476  ipolub  49478  ipoglblem  49479  ipoglb  49481  oppcendc  49508  oppcthinendcALT  49931  functhinclem2  49935  fullthinc  49940  fullthinc2  49941  euendfunc  50016  bnd2d  50171  setrec1lem1  50177  setrec1lem4  50180  setrec2fun  50182