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 282	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbi12  349  ifpbi123d  1095  nfbiit  1881  nfbidv  1952  sbjust  2095  nfbidf  2260  cbvsbvf  2395  drnf1v  2403  drnf1  2475  mo4  2594  cbvmovw  2630  cbvmow  2631  axextg  2737  rspw  3242  cbvralvw  3243  cbvralfw  3305  raleqbidv  3338  cbvraldva2  3340  sbralie  3342  sbralieOLD  3344  cbvralf  3349  ralcom2  3366  vtoclgaf  3540  vtoclga  3541  rspct  3567  rspc  3569  rspc2gv  3591  rexraleqim  3606  ralab2  3660  nelrdva  3668  mob2  3678  mob  3680  morex  3682  reu7  3695  reu8  3696  reu2eqd  3699  cdeqim  3736  sbcimg  3792  sbcim1  3797  sbceqal  3805  csbhypf  3881  cbvralcsf  3895  dfssf  3928  reldisj  4413  ralidmw  4477  reusngf  4640  rexreusng  4645  reuprg0  4668  elpreqpr  4832  unissb  4906  intss1  4928  intmin  4933  dftr2c  5221  trel  5226  zfpow  5337  reusv2lem4  5372  reusv3i  5375  rext  5429  opth  5458  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  poeq1  5572  pocl  5577  swopolem  5579  swopo  5580  isso2i  5606  vtoclr  5724  poinxp  5742  posn  5747  ssrel  5769  ssrel2  5771  ssrelrel  5782  relop  5836  cotrg  6111  cnvsym  6114  reu3op  6293  reuop  6294  dfpo2  6297  preddowncl  6333  frpoinsg  6344  ordelord  6382  iota5  6519  dffun2  6546  sbcfung  6560  funopg  6570  brprcneu  6871  brprcneuALT  6872  tz6.12f  6906  funbrfv  6929  ssimaexg  6967  fvmptf  7011  fvelrn  7071  fprg  7152  dff13f  7253  f1veqaeq  7254  fpropnf1  7265  f1ounsn  7270  nf1const  7302  soisores  7325  soisoi  7326  isofrlem  7338  isopolem  7343  weniso  7352  riota5f  7395  imbrov2fvoveq  7435  oprabidw  7441  oprabid  7442  f1opr  7466  ovmpos  7558  ov2gf  7559  ov3  7573  caovcan  7614  caovordig  7615  caofrss  7713  caoftrn  7715  tfisg  7846  tfis  7847  tfisi  7851  tfindsg  7853  tfindsg2  7854  tfindes  7855  dfom2  7860  limomss  7863  nnlim  7872  peano5  7886  findsg  7890  findes  7893  resf1extb  7927  f1oweALT  7965  dfoprab4f  8049  offval22  8079  f1o2ndf1  8113  frxp  8118  poxp  8120  frpoins3xpg  8132  frpoins3xp3g  8133  poxp2  8135  frxp2  8136  xpord2indlem  8139  poxp3  8142  frxp3  8143  xpord3inddlem  8146  suppfnss  8181  onfununi  8324  smoel  8343  smogt  8350  tfrlem1  8358  tz7.48lem  8424  tz7.49  8428  oawordeu  8536  omordi  8547  oeordi  8569  nnmordi  8613  omabs  8633  nneob  8638  omsmolem  8639  qsel  8790  eroveu  8806  ecopovtrn  8814  ixpsnf1o  8932  fundmeng  9025  sbth  9081  limensuc  9138  findcard  9144  findcard2  9145  findcard2d  9147  pssnn  9149  ssfi  9153  sbthfi  9179  nneneq  9186  php  9187  unxpdom  9215  findcard3  9239  ac6sfi  9240  frfi  9241  domunfican  9277  fiint  9282  iunfi  9296  finsschain  9312  dffi3  9387  marypha1lem  9389  marypha1  9390  supeq3  9405  supeq123d  9406  supmo  9408  suplub  9416  supisolem  9430  eqinf  9441  infval  9443  infmo  9453  ordiso2  9473  ordtypelem7  9482  wemaplem1  9504  wemaplem2  9505  zfregcl  9552  zfregclOLD  9553  elirrv  9555  elirrvOLD  9556  inf0  9586  inf3lem1  9593  zfinf  9604  axinf2  9605  dfom3  9612  elom3  9613  cantnfval2  9634  cantnfle  9636  cantnflt  9637  cantnfp1lem3  9645  oemapvali  9649  cantnflem1c  9652  cantnflem1  9654  cantnf  9658  wemapwe  9662  cnfcom  9665  ttrclss  9685  ttrclselem2  9691  setind  9712  setinds  9714  frmin  9717  frinsg  9719  r1sdom  9742  r1ordg  9746  rankonidlem  9796  rankunb  9818  scottabf  9862  bnd2  9875  infxpenlem  9993  infxpenc2  10002  dfac8alem  10009  dfac8clem  10012  indcardi  10021  alephordi  10054  alephinit  10075  alephfp  10088  aceq3lem  10100  dfac5lem4  10106  dfac5  10108  dfac2b  10110  dfac9  10116  dfac12lem2  10124  dfac12lem3  10125  kmlem1  10130  kmlem4  10133  kmlem10  10139  kmlem12  10141  kmlem13  10142  pwsdompw  10182  ackbij1lem16  10213  cfslb2n  10247  cfsmolem  10249  sornom  10256  fin2i  10274  infpssrlem4  10285  isfin2-2  10298  isfin3ds  10308  fin23lem17  10317  fin23lem32  10323  fin23lem34  10325  fin23lem35  10326  fin23lem39  10329  fin23lem41  10331  isf32lem2  10333  isf33lem  10345  isf34lem4  10356  isf34lem6  10359  fin1a2lem10  10388  axcc2lem  10415  axcc3  10417  axcc4dom  10420  dominf  10424  axdc2lem  10427  axdc3lem2  10430  ac6sg  10467  zorn2lem7  10481  zornn0g  10484  ttukeylem5  10492  ttukeylem6  10493  axdclem  10498  dominfac  10553  axrepndlem1  10572  axrepndlem2  10573  axunndlem1  10575  axunnd  10576  axpowndlem2  10578  axpowndlem3  10579  axpowndlem4  10580  axregndlem2  10583  axregnd  10584  axinfndlem1  10585  axinfnd  10586  axacndlem4  10590  axacndlem5  10591  axacnd  10592  zfcndpow  10596  zfcndinf  10598  fpwwe2lem4  10614  fpwwe2lem7  10617  fpwwe2lem11  10621  pwfseqlem4a  10641  pwfseqlem4  10642  pwfseqlem5  10643  pwfseq  10644  wunfi  10701  wunex2  10718  inar1  10755  rankcf  10757  tskord  10760  grudomon  10797  grur1a  10799  axgroth6  10808  axgroth3  10811  axgroth4  10812  eltskm  10823  indpi  10887  pinq  10907  nqereu  10909  prcdnq  10973  prnmax  10975  ltsopr  11012  prlem936  11027  ltsosr  11074  recexsrlem  11083  mulgt0sr  11085  map2psrpr  11090  supsrlem  11091  axrrecex  11143  axpre-lttrn  11146  axpre-mulgt0  11148  axpre-sup  11149  axsup  11280  dedekind  11368  ltordlem  11734  ltord1  11735  wloglei  11741  squeeze0  12113  infm3  12169  nnsub  12275  nnunb  12495  peano5uzti  12681  fzind  12689  uzind4s  12927  uzind4s2  12928  zmax  12964  zbtwnre  12965  xmulasslem  13306  xrsupsslem  13328  xrinfmsslem  13329  xrub  13333  infmremnf  13365  injresinj  13816  om2uzlti  13982  uzindi  14014  axdc4uz  14016  ssnn0fi  14017  rabssnn0fi  14018  suppssfz  14026  seqp1  14048  seqcl2  14052  seqfveq2  14056  seqshft2  14060  monoord  14064  seqsplit  14067  seqf1olem2  14074  seqf1o  14075  seqid2  14080  seqhomo  14081  seqof2  14092  expcl2lem  14105  facdiv  14319  facwordi  14321  faclbnd4lem2  14326  hashnn0n0nn  14423  hashf1lem2  14489  seqcoll  14497  fi1uzind  14540  brfi1indALT  14543  wrdind  14755  wrd2ind  14756  swrdccatin1  14758  swrdccat3blem  14772  reuccatpfxs1lem  14779  repswccat  14819  cshf1  14843  trclfvcotr  15042  relexprelg  15071  rtrclreclem4  15094  relexpindlem  15096  ello1mpt  15568  o1co  15633  o1compt  15634  rlimcn3  15637  climcn2  15640  subcn2  15642  o1of2  15660  fsumclf  15785  fsumsplitf  15789  fsumsplit1  15792  fsum2d  15818  modfsummod  15842  fsumabs  15849  telfsumo  15850  fsumrlim  15859  fsumo1  15860  o1fsum  15861  fsumiun  15869  prodfdiv  15946  fprod2d  16031  fproddivf  16037  fprodsplitf  16038  fprodsplit1f  16040  rpnnen2lem10  16274  sqrt2irr  16300  dvdsle  16363  divalglem7  16452  divalglem8  16453  ndvdssub  16462  gcdcllem1  16552  dfgcd2  16599  algcvg  16629  algcvga  16632  algfx  16633  lcmgcdlem  16659  lcmdvds  16661  lcmf  16686  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem  16694  lcmfdvds  16695  lcmfun  16698  coprmgcdb  16702  coprmdvds1  16705  coprmdvds2  16707  coprmprod  16714  coprmproddvds  16716  prmind2  16738  dvdsprime  16740  nprm  16741  dvdsprm  16757  exprmfct  16758  coprm  16765  isprm6  16768  prmfac1  16774  eulerthlem2  16836  pcqmul  16908  pcqcl  16911  pc2dvds  16934  pcz  16936  prmpwdvds  16959  infpn2  16968  vdwlem12  17047  ramub2  17069  rami  17070  ramcl  17084  prmdvdsprmop  17098  prmlem0  17160  mreintcl  17642  ismred2  17650  mrissmrcd  17691  mreexexlemd  17695  iscatd2  17732  moni  17788  yoniso  18336  isprs  18347  prslem  18348  drsdirfi  18356  ispos  18365  posi  18368  isposd  18373  pospropd  18376  lubfval  18399  lublecllem  18409  glbfval  18412  joinle  18435  meetle  18449  poslubmo  18460  posglbmo  18461  resspos  18480  lubl  18563  lubun  18566  clatleglb  18569  ipodrsima  18592  acsdrsel  18594  isacs4lem  18595  isacs5lem  18596  acsdrscl  18597  mreclatBAD  18614  pslem  18623  dirtr  18653  chnind  18672  mndind  18882  mhmlem  19123  isnsg2  19217  ghmf1  19311  orbsta  19378  symgextf1  19486  gsmsymgrfix  19493  gsmsymgreq  19497  symggen  19535  psgnunilem4  19562  sylow1lem1  19663  sylow2alem2  19683  sylow2a  19684  lsmmod  19740  lsmdisj2  19747  efgsrel  19799  efgredlemd  19809  efgredlem  19812  efgred  19813  gsumzaddlem  19986  gsummptnn0fz  20051  gsummptnn0fzfv  20052  telgsumfzs  20054  telgsums  20058  dprdval  20070  dprddisj2  20106  ablfac1eulem  20139  pgpfac1lem1  20141  pgpfac1lem5  20146  pgpfac1  20147  pgpfaclem2  20149  pgpfac  20151  isomnd  20188  omndadd  20193  gsumle  20210  irredmul  20507  islring  20639  lringuplu  20643  rrgval  20796  rrgeq0i  20798  isdomn  20804  domneq0  20807  isdomn4  20814  domnlcanb  20818  domnrcanb  20820  isdrngrd  20869  isdrngrdOLD  20871  sdrgacs  20904  isorng  20964  orngmul  20968  islbs3  21279  rngqiprngimf1lem  21434  isprmidl  21463  prmidl  21465  prmidlc  21473  prmidlprop  21476  ssdifidlprm  21486  cnsubrglem  21567  prmirredlem  21622  znfld  21710  znrrg  21715  cygznlem3  21719  isphl  21778  ipeq0  21788  isphld  21804  phlpropd  21805  lsmcss  21842  frlmphl  21931  frlmup1  21948  lindfrn  21971  islindf4  21988  islindf5  21989  mplsubglem  22148  mpllsslem  22149  mplcoe1  22188  mplcoe5  22191  mpfind  22266  ismhp3  22305  coe1fzgsumd  22464  gsummoncoe1  22468  pf1ind  22515  evl1gsumd  22517  dmatelnd  22653  mat1scmat  22696  mdetdiaglem  22755  mdetralt  22765  mdetralt2  22766  mdetunilem1  22769  mdetunilem2  22770  mdetunilem3  22771  mdetunilem4  22772  mdetunilem9  22777  smadiadetr  22832  pmatcoe1fsupp  22858  mp2pm2mplem4  22966  uniopn  23054  fiinopn  23058  epttop  23166  clsndisj  23232  elcls3  23240  neiptoptop  23288  neiptopnei  23289  cnpval  23393  iscnp  23394  cnpimaex  23413  lmcvg  23419  cnprest  23446  cnprest2  23447  lmss  23455  lmff  23458  t0sep  23481  hausnei  23485  isnrm2  23515  t1sep2  23526  isreg2  23534  iscmp  23545  cmpcov  23546  cmpsublem  23556  cmpsub  23557  tgcmp  23558  uncmp  23560  fiuncmp  23561  hauscmplem  23563  cmpfi  23565  cmpfii  23566  dfconn2  23576  connsuba  23577  connsub  23578  nconnsubb  23580  1stcclb  23601  1stcfb  23602  2ndc1stc  23608  1stcrest  23610  1stcelcls  23618  restnlly  23639  lly1stc  23653  comppfsc  23689  kgenval  23692  kgeni  23694  kgencn2  23714  ptcldmpt  23771  ptclsg  23772  dfac14lem  23774  dfac14  23775  txcnp  23777  ptcnp  23779  hausdiag  23802  txlm  23805  tx1stc  23807  xkococn  23817  cnmpt12  23824  cnmpt22  23831  kqt0lem  23893  isr0  23894  regr1lem2  23897  kqreglem1  23898  r0sep  23905  ptcmpfi  23970  elmptrab  23984  isfil  24004  filss  24010  isufil2  24065  cfinufil  24085  rnelfm  24110  fmfnfmlem2  24112  fmfnfmlem4  24114  flimopn  24132  flimrest  24140  flftg  24153  cnpflf  24158  txflf  24163  fclsopni  24172  fclsrest  24181  fclscf  24182  flimfnfcls  24185  fcfnei  24192  alexsublem  24201  alexsubb  24203  alexsubALTlem3  24206  alexsubALTlem4  24207  alexsubALT  24208  cnextcn  24224  cnextfres1  24225  tgpt0  24276  qustgplem  24278  tsmsi  24291  tsmssubm  24300  tsmsres  24301  tsmsf1o  24302  tsmsxp  24312  ustssel  24363  ust0  24377  ustuqtop4  24401  ucnima  24437  ucncn  24441  iscusp  24455  cuspcvg  24457  imasdsf1olem  24530  blssps  24581  blss  24582  metss  24665  comet  24670  metcnp3  24697  metcnp2  24699  txmetcnp  24704  metuel2  24722  metucn  24728  nrmmetd  24731  nlmvscn  24844  nrginvrcn  24849  nmolb  24874  xrge0tsms  24992  mpomulcn  25026  divcn  25027  fsumcn  25029  elcncf2  25049  cncfi  25053  mulc1cncf  25064  cncfmet  25068  xrhmeo  25105  bndth  25117  nmoleub2lem2  25275  nmoleub3  25278  ipcn  25405  lmmbr  25417  caucfil  25442  pmltpc  25609  ovolfiniun  25660  ovolicc2lem3  25678  ovolicc2  25681  mblsplit  25691  finiunmbl  25703  volfiniun  25706  voliunlem3  25711  ioorinv  25735  ioorcl  25736  dyadmax  25757  dyadmbllem  25758  dyadmbl  25759  opnmbllem  25760  volcn  25765  vitalilem2  25768  vitalilem3  25769  vitali  25772  i1fd  25840  itg2seq  25901  itg2addlem  25917  itgfsum  25986  ellimc3  26038  dvbsss  26061  dvnres  26090  dvmptfsum  26134  dvferm1lem  26143  dvferm2lem  26145  rolle  26149  c1lip1  26156  lhop1lem  26172  lhop1  26173  dvfsumlem2  26186  dvfsumlem4  26188  dvfsumrlim  26190  dvfsum2  26193  ftc1a  26196  ftc1lem6  26200  mdegleb  26221  mdeglt  26222  deg1leb  26252  deg1lt  26254  ply1divex  26294  fta1glem2  26326  fta1g  26327  plyco0  26349  plyeq0lem  26367  coeeq2  26399  dgrle  26400  dgrcolem2  26431  dgrco  26432  plydivlem4  26457  plydivex  26458  fta1lem  26468  fta1  26469  vieta1lem2  26472  vieta1  26473  aalioulem2  26496  aalioulem4  26498  abelth  26604  cxpcn3  26913  rlimcnp  27130  xrlimcnp  27133  cxploglim  27142  scvxcvx  27150  jensen  27153  lgamgulmlem2  27194  wilthlem2  27233  wilthlem3  27234  fta  27244  mpodvdsmulf1o  27358  dvdsmulf1o  27360  perfectlem2  27394  dchrelbas3  27402  dchrelbas4  27407  dchrn0  27414  bcmono  27441  lgsdir2lem4  27492  lgsdchr  27519  gausslemma2dlem0i  27528  lgseisenlem2  27540  lgsquad2lem2  27549  2sqlem6  27587  2sqlem8  27590  2sqlem10  27592  dchrisumlema  27652  dchrisumlem2  27654  dchrisumlem3  27655  nosupprefixmo  27864  noinfprefixmo  27865  nosupcbv  27866  nosupdm  27868  nosupfv  27870  nosupres  27871  nosupbnd1lem1  27872  nosupbnd1lem3  27874  nosupbnd1lem5  27876  nosupbnd2  27880  noinfcbv  27881  noinfdm  27883  noinffv  27885  noinfres  27886  noinfbnd1lem1  27887  noinfbnd1lem3  27889  noinfbnd1lem5  27891  noinfbnd2  27895  nocvxminlem  27947  madebdaylemold  28091  madebdaylemlrcut  28092  madebday  28093  lrrecpo  28134  addsproplem1  28162  addsprop  28169  leadds1  28182  negsproplem1  28221  negsprop  28228  mulsproplemcbv  28308  mulsproplem1  28309  mulsprop  28323  precsexlem8  28407  precsexlem9  28408  precsexlem11  28410  precsex  28411  bdayons  28469  addonbday  28472  onsfi  28549  n0subs  28556  oldfib  28570  eln0zs  28593  bdaypw2n0bndlem  28656  bdaypw2n0bnd  28657  bdayfinbndcbv  28659  bdayfinbndlem1  28660  bdayfinbndlem2  28661  bdayfinbnd  28662  istrkgb  28724  istrkgcb  28725  istrkge  28726  axtgcgrid  28732  axtg5seg  28734  axtgbtwnid  28735  axtgpasch  28736  axtgcont1  28737  axtgeucl  28741  iscgrglt  28783  tgcgr4  28800  axcgrtr  29265  gropd  29381  grstructd  29382  upgredg2vtx  29491  upgredgpr  29492  edglnl  29493  numedglnl  29494  usgredg2vtxeuALT  29572  nbgr2vtx1edg  29700  finsumvtxdg2size  29900  wlkp1lem8  30028  upgrwlkdvdelem  30085  usgr2wlkneq  30105  usgr2pthlem  30112  pthdlem2lem  30116  uspgrn2crct  30157  2pthdlem1  30279  eleclclwwlkn  30427  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  3pthdlem1  30515  eupth2  30590  frgr3vlem1  30624  3vfriswmgrlem  30628  frgrwopreglem4a  30661  frgr2wwlk1  30680  wlkl0  30718  numclwlk2lem2f1o  30730  friendshipgt3  30749  eulplig  30837  nvz  31021  nmobndseqi  31131  nmobndseqiALT  31132  nmlno0  31147  blocnilem  31156  dipdir  31194  dipass  31197  siilem2  31204  ubthlem2  31223  ubth  31225  htth  31270  normpyth  31497  norm3lemt  31504  chlimi  31586  chcompl  31594  omlsii  31755  pjoml  31788  h1de2i  31905  elspansn2  31919  h1datom  31934  pjoml2  31963  pjoml3  31964  lecm  31969  chscllem2  31990  osum  31997  spansncv  32005  pjcjt2  32044  pjopyth  32072  eigre  32187  eigorth  32190  hhcno  32256  hhcnf  32257  cnopc  32265  cnfnc  32282  nmcexi  32378  nmcopexi  32379  nmcfnexi  32403  pjssge0i  32518  hstel2  32571  stj  32587  stri  32609  hstri  32617  stcltr1i  32626  mdbr  32646  mdi  32647  mdbr3  32649  mdbr4  32650  dmdbr  32651  dmdmd  32652  dmdi  32654  dmdbr3  32657  dmdbr4  32658  dmdbr5  32660  mdsl1i  32673  mdslmd1lem3  32679  mdslmd1lem4  32680  mdslmd1i  32681  csmdsymi  32686  cvmd  32688  atss  32698  atom1d  32705  chcv1  32707  hatomic  32712  atord  32740  atcvat2  32741  mddmdin0i  32783  opreu2reuALT  32823  rmoxfrd  32839  ifeqeqx  32888  ssiun2sf  32904  iinabrex  32914  ssrelf  32960  fmptcof2  33002  acunirnmpt  33004  acunirnmpt2  33005  acunirnmpt2f  33006  aciunf1lem  33007  suppovss  33026  fz1nntr  33147  nn0min  33165  fsumiunle  33173  wrdt2ind  33273  ressprs  33286  toslublem  33292  tosglblem  33294  mntoval  33302  ismntd  33304  dfmgc2lem  33315  dfmgc2  33316  xrge0tsmsd  33393  fzto1st  33423  psgnfzto1st  33425  submarchi  33506  archirng  33508  archiexdiv  33510  archiabllem1a  33511  archiabllem2a  33514  archiabl  33518  isarchiofld  33519  gsumvsca1  33546  gsumvsca2  33547  elrgspnlem4  33565  domnpropd  33600  linds2eq  33694  ismxidl  33745  mxidlmax  33748  rprmval  33806  isrprm  33807  rprmdvds  33809  rprmdvdsprod  33824  1arithidomlem1  33825  1arithidom  33827  1arithufdlem3  33836  dfufd2lem  33839  lbsdiflsp0  34016  fedgmullem1  34019  fedgmullem2  34020  fldext2chn  34118  constrmon  34134  submateq  34199  lmatfval  34204  lmatcl  34206  iscref  34234  crefi  34237  pcmplfin  34250  xrge0iifiso  34325  esumcvg  34476  esum2dlem  34482  sigaclcu  34507  sigaclci  34522  unelsiga  34524  unelldsys  34548  sigapildsys  34552  ldgenpisyslem1  34553  fiunelros  34564  measvun  34599  measiun  34608  carsgmon  34704  carsgsigalem  34705  carsgclctunlem2  34709  carsgclctun  34711  pmeasmono  34714  pmeasadd  34715  sibfof  34730  sitgclg  34732  eulerpartlemgvv  34766  signsply0  34938  signstfvneq0  34959  breprexp  35020  hgt749d  35036  istrkg2d  35053  axtgupdim2ALTV  35055  bnj1385  35220  bnj110  35246  bnj222  35271  bnj229  35272  bnj590  35298  bnj865  35311  bnj849  35313  bnj981  35338  bnj1014  35349  bnj1015  35350  bnj1112  35371  bnj1118  35372  bnj1123  35374  bnj1128  35378  bnj1125  35380  bnj1148  35384  bnj1154  35387  bnj1326  35414  bnj1384  35420  bnj1489  35444  bnj1497  35448  funen1cnv  35477  r1filimi  35497  trssfir1om  35507  r1omhfb  35508  setindregs  35543  trssfir1omregs  35549  r1omhfbregs  35550  axpowg  35559  onvf1odlem2  35588  f1resfz0f1d  35605  cplgredgex  35613  acycgrcycl  35639  subfacp1lem6  35677  erdszelem9  35691  kur14lem9  35706  sconnpht  35721  cvmsss2  35766  cvmliftlem7  35783  cvmliftlem10  35786  fmlasuc  35878  gonar  35887  goalr  35889  mclsrcl  36053  mclsssvlem  36054  mclsval  36055  mclsax  36061  mclsind  36062  mclsppslem  36075  iota5f  36216  fununiq  36261  dfon2lem3  36275  dfon2lem4  36276  dfon2lem5  36277  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  dfon2  36282  btwnconn1lem11  36589  linethru  36645  fwddifnp1  36657  rankelg  36660  rankeq1o  36663  sbequbidv  36726  cbvralvw2  36738  cbvmodavw  36762  cbvsbdavw  36766  cbvsbdavw2  36767  subtr  36825  subtr2  36826  trer  36827  nn0prpwlem  36833  nn0prpw  36834  neibastop2lem  36871  filnetlem4  36892  axtco1from2  36986  axtcond  36989  axuntco  36990  dfttc4lem2  37040  dfttc4  37041  mh-setindnd  37048  regsfromregtco  37049  regsfromsetind  37050  mh-inf3f1  37052  mh-unprimbi  37055  mh-infprim2bi  37058  bj-hbxfrbi  37235  bj-hbyfrbi  37236  bj-ssblem1  37276  bj-ssblem2  37277  bj-ax12  37279  irrdiff  37970  relowlssretop  38009  rdgeqoa  38016  rdgssun  38024  exrecfnlem  38025  finxpreclem6  38042  pibp19  38060  pibt2  38063  wl-ax12v2cl  38152  wl-mo3t  38231  wl-sb8mot  38235  wl-sb8motv  38236  finixpnum  38256  matunitlindflem1  38267  ptrest  38270  poimirlem13  38284  poimirlem14  38285  poimirlem17  38288  poimirlem18  38289  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  poimirlem24  38295  poimirlem25  38296  poimirlem26  38297  poimirlem28  38299  poimirlem30  38301  poimirlem31  38302  poimirlem32  38303  poimir  38304  heicant  38306  mblfinlem1  38308  mblfinlem2  38309  mblfinlem3  38310  voliunnfl  38315  volsupnfl  38316  mbfresfi  38317  itg2addnclem3  38324  ftc1cnnc  38343  ftc1anclem7  38350  ftc1anc  38352  sdclem2  38393  fdc  38396  fdc1  38397  neificl  38404  mettrifi  38408  sstotbnd2  38425  cntotbnd  38447  heibor1lem  38460  bfp  38475  isass  38497  ismgmOLD  38501  isexid2  38506  iscringd  38649  ispridl  38685  pridl  38688  ismaxidl  38691  maxidlmax  38694  ispridlc  38721  pridlc  38722  dmnnzd  38726  relcnveq2  38978  ecin0  39001  elrelscnveq2  39278  elsymrels3  39287  eltrrels3  39313  eleqvrels3  39326  eqvrelqsel  39349  disjimeceqim2  39454  eldisjim3  39464  eldisjlem19  39562  eldisjsim3  39586  axc11n-16  39712  ax12eq  39715  ax12el  39716  ax12inda  39722  ax12v2-o  39723  fsumshftd  39726  riotasv2d  39731  lshpdisj  39761  lsmsatcv  39784  lsat0cv  39807  lcvexchlem4  39811  lcvexchlem5  39812  l1cvpat  39828  isopos  39954  oposlem  39956  isoml  40012  omllaw  40017  isatl  40073  atlex  40090  iscvlat  40097  cvlexch1  40102  glbconN  40151  hlsuprexch  40155  ps-1  40251  3atlem5  40261  psubspi  40521  llnexchb2  40643  elpcliN  40667  pclfinclN  40724  ldilval  40887  ltrnfset  40891  ltrnset  40892  ltrnu  40895  trlfset  40934  trlset  40935  trlval2  40937  cdleme25cv  41132  cdleme31so  41153  cdleme31fv  41164  cdlemefrs29bpre0  41170  cdleme32fva  41211  cdleme40v  41243  trlord  41343  cdlemkid3N  41707  cdlemkid4  41708  dihffval  42004  dihfval  42005  dihval  42006  lpolconN  42261  mapdordlem2  42411  hdmapfval  42601  hdmapval  42602  hdmapval2  42606  aks4d1p7  42850  isprimroot  42860  primrootlekpowne0  42872  sticksstones1  42913  sticksstones2  42914  sticksstones10  42922  sticksstones12a  42924  aks6d1c6lem3  42939  indstrd  42960  unitscyglem2  42963  unitscyglem3  42964  unitscyglem4  42965  nnn1suc  43033  fsuppind  43322  eu6w  43408  ismrcd1  43429  ismrcd2  43430  ismrc  43432  isnacs3  43441  nacsfix  43443  mzpcompact2  43483  fphpd  43543  fphpdo  43544  monotuz  43668  monotoddzzfi  43669  monotoddzz  43670  oddcomabszz  43671  zindbi  43673  setindtrs  43752  dford3lem2  43754  ttac  43763  dnnumch1  43771  fnwe2lem2  43778  aomclem3  43783  aomclem6  43786  aomclem8  43788  dfac11  43789  dfac21  43793  islssfg2  43798  hbtlem5  43855  hbt  43857  flcidc  43897  mendlmod  43916  unielss  43945  rababg  44300  elmapintrab  44302  iunrelexpuztr  44445  frege92  44681  frege104  44693  ntrkbimka  44764  ntrk0kbimka  44765  neik0pk1imk0  44773  isotone1  44774  isotone2  44775  ntrclsiso  44793  ntrclskb  44795  ntrneiiso  44817  ntrneik3  44822  ntrneix3  44823  gneispacess2  44872  grur1cld  44956  ismnu  44971  mnuop23d  44976  mnuunid  44987  ismnushort  45011  dvgrat  45022  cvgdvgrat  45023  binomcxplemnotnn0  45066  pm14.122b  45133  sbiota1  45144  relprel  45660  relpfrlem  45662  modelaxreplem1  45687  modelaxreplem2  45688  modelaxrep  45690  omssaxinf2  45697  modelac8prim  45701  permaxinf2lem  45721  permac8prim  45723  nregmodel  45726  fnchoice  45749  fiiuncl  45785  iunincfi  45812  disjf1  45901  wessf1ornlem  45903  disjinfi  45910  axccdom  45938  dmrelrnrel  45942  axccd  45944  monoords  46016  fperiodmullem  46022  supxrgere  46049  supxrgelem  46053  supxrge  46054  xrlexaddrp  46068  infxr  46082  infleinf  46087  supxrleubrnmptf  46165  monoordxrv  46195  monoordxr  46196  monoord2xr  46198  fsummulc1f  46287  fsumnncl  46288  fsumf1of  46290  fsumreclf  46292  fsumlessf  46293  fsumsermpt  46295  fmul01  46296  fmulcl  46297  fmuldfeqlem1  46298  fmuldfeq  46299  fmul01lt1lem1  46300  fmul01lt1lem2  46301  fprodexp  46310  fprodabs2  46311  fprodcnlem  46315  climmulf  46320  climexp  46321  climsuse  46324  climrecf  46325  climinff  46327  climaddf  46331  mullimc  46332  mullimcf  46339  limcperiod  46344  sumnnodd  46346  lptre2pt  46354  limsupre  46355  neglimc  46361  addlimc  46362  0ellimcdiv  46363  limclner  46365  climsubmpt  46374  climreclf  46378  climeldmeqmpt  46382  climfveqmpt  46385  fnlimfvre  46388  climfveqf  46394  climfveqmpt3  46396  climeldmeqf  46397  limsupref  46399  limsupbnd1f  46400  climeqf  46402  climeldmeqmpt3  46403  climinf2  46421  limsupubuz  46427  climinf2mpt  46428  climinfmpt  46429  limsupmnf  46435  limsupequz  46437  limsupre2  46439  limsupequzmptf  46445  limsupre3  46447  lmbr3  46461  cnrefiisp  46544  xlimxrre  46545  xlimmnfvlem1  46546  xlimpnfvlem1  46550  climxlim2lem  46559  cncfshift  46588  cncfperiod  46593  icccncfext  46601  fprodcncf  46614  fperdvper  46633  dvmptmulf  46651  dvnmptdivc  46652  dvnmul  46657  dvmptfprod  46659  dvnprodlem1  46660  dvnprodlem2  46661  dvnprodlem3  46662  iblspltprt  46687  itgspltprt  46693  stoweidlem3  46717  stoweidlem4  46718  stoweidlem6  46720  stoweidlem8  46722  stoweidlem15  46729  stoweidlem16  46730  stoweidlem17  46731  stoweidlem19  46733  stoweidlem20  46734  stoweidlem22  46736  stoweidlem23  46737  stoweidlem26  46740  stoweidlem27  46741  stoweidlem30  46744  stoweidlem31  46745  stoweidlem32  46746  stoweidlem34  46748  stoweidlem35  46749  stoweidlem42  46756  stoweidlem43  46757  stoweidlem48  46762  stoweidlem50  46764  stoweidlem51  46765  stoweidlem57  46771  stoweidlem59  46773  stoweidlem62  46776  wallispilem3  46781  dirkercncflem2  46818  fourierdlem11  46832  fourierdlem12  46833  fourierdlem15  46836  fourierdlem16  46837  fourierdlem21  46842  fourierdlem34  46855  fourierdlem41  46862  fourierdlem42  46863  fourierdlem46  46866  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem51  46871  fourierdlem68  46888  fourierdlem71  46891  fourierdlem72  46892  fourierdlem73  46893  fourierdlem76  46896  fourierdlem79  46899  fourierdlem81  46901  fourierdlem83  46903  fourierdlem86  46906  fourierdlem89  46909  fourierdlem90  46910  fourierdlem91  46911  fourierdlem92  46912  fourierdlem94  46914  fourierdlem97  46917  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fourierdlem112  46932  fourierdlem113  46933  etransclem2  46950  etransclem46  46994  salunicl  47030  saluncl  47031  intsaluni  47043  dfsalgen2  47055  sge0f1o  47096  sge0lempt  47124  sge0iunmptlemfi  47127  sge0p1  47128  sge0fodjrnlem  47130  sge0iunmpt  47132  sge0ltfirpmpt2  47140  sge0isummpt2  47146  sge0xaddlem2  47148  sge0xadd  47149  nnfoctbdjlem  47169  meadjuni  47171  meadjiun  47180  voliunsge0lem  47186  meaiuninclem  47194  meaiunincf  47197  meaiuninc3v  47198  meaiuninc3  47199  meaiininclem  47200  meaiininc  47201  omeunile  47219  isomenndlem  47244  ovn0lem  47279  ovnsubaddlem1  47284  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvlelem4  47312  hoidmvle  47314  hspmbllem2  47341  hoimbl2  47379  vonhoire  47386  vonicclem2  47398  vonn0ioo2  47404  vonn0icc2  47406  salpreimagelt  47421  salpreimalegt  47423  pimdecfgtioc  47429  pimincfltioc  47430  pimincfltioo  47432  salpreimagtge  47439  salpreimaltle  47440  salpreimagtlt  47444  incsmf  47456  decsmf  47481  smflimlem1  47485  smflimlem2  47486  smflimlem3  47487  smflimlem4  47488  smfpimcclem  47521  funressnmo  47783  fcoresf1  47806  aiota0def  47833  euoreqb  47846  2reu8i  47850  2reuimp0  47851  funressndmafv2rn  47960  funressnbrafv2  47981  funbrafv2  47984  smonoord  48114  elsetpreimafvbi  48140  iccpartgt  48176  iccelpart  48182  iccpartiun  48183  icceuelpartlem  48184  icceuelpart  48185  iccpartnel  48187  fargshiftf1  48190  ichexmpl2  48219  ichnreuop  48221  ichreuopeq  48222  sprsymrelfolem2  48242  prproropf1olem4  48255  paireqne  48260  reupr  48271  reuopreuprim  48275  fmtnofac2  48321  fmtnofac1  48322  prmdvdsfmtnof1lem2  48337  perfectALTVlem2  48487  nfermltl8rev  48507  nfermltl2rev  48508  sbgoldbwt  48542  sbgoldbst  48543  sgoldbeven3prm  48548  sbgoldbm  48549  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  evengpop3  48563  evengpoap3  48564  bgoldbnnsum3prm  48569  bgoldbtbndlem4  48573  bgoldbtbnd  48574  tgblthelfgott  48580  tgoldbach  48582  grimuhgr  48652  grimcnv  48653  isuspgrimlem  48660  isubgr3stgrlem4  48734  isubgr3stgrlem6  48736  isubgr3stgrlem7  48737  gpgedg2ov  48831  gpgedg2iv  48832  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  pgnbgreunbgrlem5lem1  48885  pgnbgreunbgrlem5lem2  48886  pgnbgreunbgrlem5lem3  48887  pgnbgreunbgr  48890  idomnzd  49111  ply1mulgsumlem2  49167  islininds  49226  linindslinci  49228  lindslinindsimp1  49237  linds0  49245  lindsrng01  49248  snlindsntorlem  49250  snlindsntor  49251  ldepsnlinc  49288  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  nn0sumshdiglem1  49401  nn0sumshdiglem2  49402  nn0sumshdig  49403  itschlc0yqe  49540  f1mo  49631  iscnrm3lem5  49715  iscnrm3r  49726  isprsd  49733  lubeldm2d  49736  glbeldm2d  49737  joindm2  49746  meetdm2  49748  ipolublem  49764  ipolub  49766  ipoglblem  49767  ipoglb  49769  oppcendc  49796  oppcthinendcALT  50219  functhinclem2  50223  fullthinc  50228  fullthinc2  50229  euendfunc  50304  bnd2d  50459  setrec1lem1  50465  setrec1lem4  50468  setrec2fun  50470  alsbid  50580  cbvals  50583