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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12  349  ifpbi123d  1095  nfbiit  1884  nfbidv  1955  sbjust  2098  nfbidf  2263  cbvsbvf  2397  drnf1v  2405  drnf1  2477  mo4  2596  cbvmovw  2632  cbvmow  2633  axextg  2739  rspw  3244  cbvralvw  3245  cbvralfw  3307  raleqbidv  3340  cbvraldva2  3342  sbralie  3344  sbralieOLD  3346  cbvralf  3351  ralcom2  3368  vtoclgaf  3542  vtoclga  3543  rspct  3569  rspc  3571  rspc2gv  3593  rexraleqim  3608  ralab2  3662  nelrdva  3670  mob2  3680  mob  3682  morex  3684  reu7  3697  reu8  3698  reu2eqd  3701  cdeqim  3738  sbcimg  3794  sbcim1  3799  sbceqal  3807  csbhypf  3882  cbvralcsf  3896  dfssf  3929  reldisj  4413  ralidmw  4479  reusngf  4642  rexreusng  4647  reuprg0  4670  elpreqpr  4834  unissb  4908  intss1  4930  intmin  4935  dftr2c  5223  trel  5228  zfpow  5339  reusv2lem4  5374  reusv3i  5377  rext  5431  opth  5460  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  poeq1  5574  pocl  5579  swopolem  5581  swopo  5582  isso2i  5608  vtoclr  5726  poinxp  5744  posn  5749  ssrel  5771  ssrel2  5773  ssrelrel  5784  relop  5838  cotrg  6113  cnvsym  6116  reu3op  6297  reuop  6298  dfpo2  6301  preddowncl  6337  frpoinsg  6348  ordelord  6386  iota5  6523  dffun2  6550  sbcfung  6564  funopg  6574  brprcneu  6875  brprcneuALT  6876  tz6.12f  6910  funbrfv  6933  ssimaexg  6971  fvmptf  7015  fvelrn  7075  fprg  7158  dff13f  7258  f1veqaeq  7259  fpropnf1  7270  f1ounsn  7279  nf1const  7311  soisores  7334  soisoi  7335  isofrlem  7347  isopolem  7352  weniso  7363  riota5f  7404  imbrov2fvoveq  7444  oprabidw  7450  oprabid  7451  f1opr  7475  ovmpos  7567  ov2gf  7568  ov3  7582  caovcan  7624  caovordig  7625  caofrss  7723  caoftrn  7725  tfisg  7856  tfis  7857  tfisi  7861  tfindsg  7863  tfindsg2  7864  tfindes  7865  dfom2  7870  limomss  7873  nnlim  7882  peano5  7896  findsg  7900  findes  7903  resf1extb  7937  f1oweALT  7975  dfoprab4f  8059  offval22  8089  f1o2ndf1  8123  frxp  8128  poxp  8130  frpoins3xpg  8142  frpoins3xp3g  8143  poxp2  8145  frxp2  8146  xpord2indlem  8149  poxp3  8152  frxp3  8153  xpord3inddlem  8156  suppfnss  8191  onfununi  8334  smoel  8353  smogt  8360  tfrlem1  8368  tz7.48lem  8434  tz7.49  8438  oawordeu  8546  omordi  8557  oeordi  8579  nnmordi  8623  omabs  8643  nneob  8648  omsmolem  8649  qsel  8800  eroveu  8816  ecopovtrn  8824  ixpsnf1o  8942  funen1cnv  9032  fundmeng  9036  sbth  9092  limensuc  9149  findcard  9155  findcard2  9156  findcard2d  9158  pssnn  9160  ssfi  9164  sbthfi  9190  nneneq  9197  php  9198  unxpdom  9226  findcard3  9250  ac6sfi  9251  frfi  9252  domunfican  9288  fiint  9293  iunfi  9307  finsschain  9323  dffi3  9398  marypha1lem  9400  marypha1  9401  supeq3  9416  supeq123d  9417  supmo  9419  suplub  9427  supisolem  9441  eqinf  9452  infval  9454  infmo  9464  ordiso2  9484  ordtypelem7  9493  wemaplem1  9515  wemaplem2  9516  zfregcl  9563  zfregclOLD  9564  elirrv  9566  elirrvOLD  9567  inf0  9597  inf3lem1  9604  zfinf  9615  axinf2  9616  dfom3  9623  elom3  9624  cantnfval2  9645  cantnfle  9647  cantnflt  9648  cantnfp1lem3  9656  oemapvali  9660  cantnflem1c  9663  cantnflem1  9665  cantnf  9669  wemapwe  9673  cnfcom  9676  ttrclss  9696  ttrclselem2  9702  setind  9723  setinds  9725  frmin  9728  frinsg  9730  r1sdom  9753  r1ordg  9757  rankonidlem  9807  rankunb  9829  scottabf  9875  bnd2  9892  infxpenlem  10013  infxpenc2  10022  dfac8alem  10029  dfac8clem  10032  indcardi  10041  alephordi  10074  alephinit  10095  alephfp  10108  aceq3lem  10120  dfac5lem4  10126  dfac5  10128  dfac2b  10130  dfac9  10136  dfac12lem2  10144  dfac12lem3  10145  kmlem1  10150  kmlem4  10153  kmlem10  10159  kmlem12  10161  kmlem13  10162  pwsdompw  10202  ackbij1lem16  10233  cfslb2n  10267  cfsmolem  10269  sornom  10276  fin2i  10294  infpssrlem4  10305  isfin2-2  10318  isfin3ds  10328  fin23lem17  10337  fin23lem32  10343  fin23lem34  10345  fin23lem35  10346  fin23lem39  10349  fin23lem41  10351  isf32lem2  10353  isf33lem  10365  isf34lem4  10376  isf34lem6  10379  fin1a2lem10  10408  axcc2lem  10435  axcc3  10437  axcc4dom  10440  dominf  10444  axdc2lem  10447  axdc3lem2  10450  ac6sg  10487  zorn2lem7  10501  zornn0g  10504  ttukeylem5  10512  ttukeylem6  10513  axdclem  10518  dominfac  10575  axrepndlem1  10594  axrepndlem2  10595  axunndlem1  10597  axunnd  10598  axpowndlem2  10600  axpowndlem3  10601  axpowndlem4  10602  axregndlem2  10605  axregnd  10606  axinfndlem1  10607  axinfnd  10608  axacndlem4  10612  axacndlem5  10613  axacnd  10614  zfcndpow  10618  zfcndinf  10620  fpwwe2lem4  10636  fpwwe2lem7  10639  fpwwe2lem11  10643  pwfseqlem4a  10663  pwfseqlem4  10664  pwfseqlem5  10665  pwfseq  10666  wunfi  10723  wunex2  10740  inar1  10777  rankcf  10779  tskord  10782  grudomon  10819  grur1a  10821  axgroth6  10830  axgroth3  10833  axgroth4  10834  eltskm  10845  indpi  10909  pinq  10929  nqereu  10931  prcdnq  10995  prnmax  10997  ltsopr  11034  prlem936  11049  ltsosr  11096  recexsrlem  11105  mulgt0sr  11107  map2psrpr  11112  supsrlem  11113  axrrecex  11165  axpre-lttrn  11168  axpre-mulgt0  11170  axpre-sup  11171  axsup  11302  dedekind  11390  ltordlem  11756  ltord1  11757  wloglei  11763  squeeze0  12135  infm3  12191  nnsub  12297  nnunb  12517  peano5uzti  12704  fzind  12712  uzind4s  12950  uzind4s2  12951  zmax  12987  zbtwnre  12988  xmulasslem  13329  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  infmremnf  13388  injresinj  13839  f1resfz0f1d  13840  om2uzlti  14006  uzindi  14038  axdc4uz  14040  ssnn0fi  14041  rabssnn0fi  14042  suppssfz  14050  seqp1  14072  seqcl2  14076  seqfveq2  14080  seqshft2  14084  monoord  14088  seqsplit  14091  seqf1olem2  14098  seqf1o  14099  seqid2  14104  seqhomo  14105  seqof2  14116  expcl2lem  14129  facdiv  14343  facwordi  14345  faclbnd4lem2  14350  hashnn0n0nn  14447  hashf1lem2  14513  seqcoll  14521  fi1uzind  14564  brfi1indALT  14567  wrdind  14783  wrd2ind  14784  swrdccatin1  14786  swrdccat3blem  14800  reuccatpfxs1lem  14807  repswccat  14849  cshf1  14873  trclfvcotr  15072  relexprelg  15101  rtrclreclem4  15124  relexpindlem  15126  ello1mpt  15598  o1co  15663  o1compt  15664  rlimcn3  15667  climcn2  15670  subcn2  15672  o1of2  15690  fsumclf  15814  fsumsplitf  15818  fsumsplit1  15821  fsum2d  15847  modfsummod  15871  fsumabs  15878  telfsumo  15879  fsumrlim  15888  fsumo1  15889  o1fsum  15890  fsumiun  15898  prodfdiv  15975  fprod2d  16060  fproddivf  16066  fprodsplitf  16067  fprodsplit1f  16069  rpnnen2lem10  16303  sqrt2irr  16329  dvdsle  16392  divalglem7  16481  divalglem8  16482  ndvdssub  16491  gcdcllem1  16581  dfgcd2  16628  algcvg  16658  algcvga  16661  algfx  16662  lcmgcdlem  16688  lcmdvds  16690  lcmf  16715  lcmfunsnlem1  16719  lcmfunsnlem2lem1  16720  lcmfunsnlem  16723  lcmfdvds  16724  lcmfun  16727  coprmgcdb  16731  coprmdvds1  16734  coprmdvds2  16736  coprmprod  16743  coprmproddvds  16745  prmind2  16767  dvdsprime  16769  nprm  16770  dvdsprm  16786  exprmfct  16787  coprm  16794  isprm6  16797  prmfac1  16803  eulerthlem2  16865  pcqmul  16937  pcqcl  16940  pc2dvds  16963  pcz  16965  prmpwdvds  16988  infpn2  16997  vdwlem12  17076  ramub2  17098  rami  17099  ramcl  17113  prmdvdsprmop  17127  prmlem0  17189  mreintcl  17671  ismred2  17679  mrissmrcd  17720  mreexexlemd  17724  iscatd2  17761  moni  17817  yoniso  18365  isprs  18376  prslem  18377  drsdirfi  18385  ispos  18394  posi  18397  isposd  18402  pospropd  18405  lubfval  18428  lublecllem  18438  glbfval  18441  joinle  18464  meetle  18478  poslubmo  18489  posglbmo  18490  resspos  18509  lubl  18592  lubun  18595  clatleglb  18598  ipodrsima  18621  acsdrsel  18623  isacs4lem  18624  isacs5lem  18625  acsdrscl  18626  mreclatBAD  18643  pslem  18652  dirtr  18682  chnind  18701  mndind  18926  degenmgm2nfun  19041  mhmlem  19174  isnsg2  19268  ghmf1  19362  orbsta  19429  symgextf1  19537  gsmsymgrfix  19544  gsmsymgreq  19548  symggen  19586  psgnunilem4  19613  sylow1lem1  19714  sylow2alem2  19734  sylow2a  19735  lsmmod  19791  lsmdisj2  19798  efgsrel  19850  efgredlemd  19860  efgredlem  19863  efgred  19864  gsumzaddlem  20037  gsummptnn0fz  20102  gsummptnn0fzfv  20103  telgsumfzs  20105  telgsums  20109  dprdval  20121  dprddisj2  20157  ablfac1eulem  20190  pgpfac1lem1  20192  pgpfac1lem5  20197  pgpfac1  20198  pgpfaclem2  20200  pgpfac  20202  isomnd  20239  omndadd  20244  gsumle  20261  irredmul  20559  islring  20691  lringuplu  20695  rrgval  20848  rrgeq0i  20850  isdomn  20856  domneq0  20859  isdomn4  20866  domnlcanb  20870  domnrcanb  20872  isdrngrd  20921  isdrngrdOLD  20923  sdrgacs  20956  isorng  21016  orngmul  21020  islbs3  21331  rngqiprngimf1lem  21486  isprmidl  21515  prmidl  21517  prmidlc  21525  prmidlprop  21528  ssdifidlprm  21538  cnsubrglem  21619  prmirredlem  21674  znfld  21762  znrrg  21767  cygznlem3  21771  isphl  21830  ipeq0  21840  isphld  21856  phlpropd  21857  lsmcss  21894  frlmphl  21983  frlmup1  22000  lindfrn  22023  islindf4  22040  islindf5  22041  mplsubglem  22200  mpllsslem  22201  mplcoe1  22240  mplcoe5  22243  mpfind  22318  ismhp3  22357  coe1fzgsumd  22516  gsummoncoe1  22520  pf1ind  22567  evl1gsumd  22569  dmatelnd  22705  mat1scmat  22748  mdetdiaglem  22807  mdetralt  22817  mdetralt2  22818  mdetunilem1  22821  mdetunilem2  22822  mdetunilem3  22823  mdetunilem4  22824  mdetunilem9  22829  smadiadetr  22884  pmatcoe1fsupp  22910  mp2pm2mplem4  23018  uniopn  23106  fiinopn  23110  epttop  23218  clsndisj  23284  elcls3  23292  neiptoptop  23340  neiptopnei  23341  cnpval  23445  iscnp  23446  cnpimaex  23465  lmcvg  23471  cnprest  23498  cnprest2  23499  lmss  23507  lmff  23510  t0sep  23533  hausnei  23537  isnrm2  23567  t1sep2  23578  isreg2  23586  iscmp  23597  cmpcov  23598  cmpsublem  23608  cmpsub  23609  tgcmp  23610  uncmp  23612  fiuncmp  23613  hauscmplem  23615  cmpfi  23617  cmpfii  23618  dfconn2  23628  connsuba  23629  connsub  23630  nconnsubb  23632  1stcclb  23653  1stcfb  23654  2ndc1stc  23660  1stcrest  23662  1stcelcls  23671  restnlly  23692  lly1stc  23706  comppfsc  23742  kgenval  23745  kgeni  23747  kgencn2  23767  ptcldmpt  23824  ptclsg  23825  dfac14lem  23827  dfac14  23828  txcnp  23830  ptcnp  23832  hausdiag  23855  txlm  23858  tx1stc  23860  xkococn  23870  cnmpt12  23877  cnmpt22  23884  kqt0lem  23946  isr0  23947  regr1lem2  23950  kqreglem1  23951  r0sep  23958  ptcmpfi  24023  elmptrab  24037  isfil  24057  filss  24063  isufil2  24118  cfinufil  24138  rnelfm  24163  fmfnfmlem2  24165  fmfnfmlem4  24167  flimopn  24185  flimrest  24193  flftg  24206  cnpflf  24211  txflf  24216  fclsopni  24225  fclsrest  24234  fclscf  24235  flimfnfcls  24238  fcfnei  24245  alexsublem  24254  alexsubb  24256  alexsubALTlem3  24259  alexsubALTlem4  24260  alexsubALT  24261  cnextcn  24277  cnextfres1  24278  tgpt0  24329  qustgplem  24331  tsmsi  24344  tsmssubm  24353  tsmsres  24354  tsmsf1o  24355  tsmsxp  24365  ustssel  24416  ust0  24430  ustuqtop4  24454  ucnima  24490  ucncn  24494  iscusp  24508  cuspcvg  24510  imasdsf1olem  24583  blssps  24634  blss  24635  metss  24718  comet  24723  metcnp3  24750  metcnp2  24752  txmetcnp  24757  metuel2  24775  metucn  24781  nrmmetd  24784  nlmvscn  24897  nrginvrcn  24902  nmolb  24927  xrge0tsms  25045  mpomulcn  25079  divcn  25080  fsumcn  25082  elcncf2  25102  cncfi  25106  mulc1cncf  25117  cncfmet  25121  xrhmeo  25158  bndth  25170  nmoleub2lem2  25328  nmoleub3  25331  ipcn  25458  lmmbr  25470  caucfil  25495  pmltpc  25662  ovolfiniun  25713  ovolicc2lem3  25731  ovolicc2  25734  mblsplit  25744  finiunmbl  25756  volfiniun  25759  voliunlem3  25764  ioorinv  25788  ioorcl  25789  dyadmax  25810  dyadmbllem  25811  dyadmbl  25812  opnmbllem  25813  volcn  25818  vitalilem2  25821  vitalilem3  25822  vitali  25825  i1fd  25893  itg2seq  25954  itg2addlem  25970  itgfsum  26039  ellimc3  26091  dvbsss  26114  dvnres  26143  dvmptfsum  26187  dvferm1lem  26196  dvferm2lem  26198  rolle  26202  c1lip1  26209  lhop1lem  26225  lhop1  26226  dvfsumlem2  26239  dvfsumlem4  26241  dvfsumrlim  26243  dvfsum2  26246  ftc1a  26249  ftc1lem6  26253  mdegleb  26274  mdeglt  26275  deg1leb  26305  deg1lt  26307  ply1divex  26347  fta1glem2  26379  fta1g  26380  plyco0  26402  plyeq0lem  26420  coeeq2  26452  dgrle  26453  dgrcolem2  26484  dgrco  26485  plydivlem4  26510  plydivex  26511  fta1lem  26521  fta1  26522  vieta1lem2  26525  vieta1  26526  aalioulem2  26549  aalioulem4  26551  abelth  26657  cxpcn3  26966  rlimcnp  27183  xrlimcnp  27186  cxploglim  27195  scvxcvx  27203  jensen  27206  lgamgulmlem2  27247  wilthlem2  27286  wilthlem3  27287  fta  27297  mpodvdsmulf1o  27411  dvdsmulf1o  27413  perfectlem2  27447  dchrelbas3  27455  dchrelbas4  27460  dchrn0  27467  bcmono  27494  lgsdir2lem4  27545  lgsdchr  27572  gausslemma2dlem0i  27581  lgseisenlem2  27593  lgsquad2lem2  27602  2sqlem6  27640  2sqlem8  27643  2sqlem10  27645  dchrisumlema  27705  dchrisumlem2  27707  dchrisumlem3  27708  nosupprefixmo  27917  noinfprefixmo  27918  nosupcbv  27919  nosupdm  27921  nosupfv  27923  nosupres  27924  nosupbnd1lem1  27925  nosupbnd1lem3  27927  nosupbnd1lem5  27929  nosupbnd2  27933  noinfcbv  27934  noinfdm  27936  noinffv  27938  noinfres  27939  noinfbnd1lem1  27940  noinfbnd1lem3  27942  noinfbnd1lem5  27944  noinfbnd2  27948  nocvxminlem  28000  madebdaylemold  28144  madebdaylemlrcut  28145  madebday  28146  lrrecpo  28187  addsproplem1  28215  addsprop  28222  leadds1  28235  negsproplem1  28274  negsprop  28281  mulsproplemcbv  28361  mulsproplem1  28362  mulsprop  28376  precsexlem8  28460  precsexlem9  28461  precsexlem11  28463  precsex  28464  bdayons  28522  addonbday  28525  onsfi  28602  n0subs  28609  oldfib  28623  eln0zs  28646  bdaypw2n0bndlem  28709  bdaypw2n0bnd  28710  bdayfinbndcbv  28712  bdayfinbndlem1  28713  bdayfinbndlem2  28714  bdayfinbnd  28715  istrkgb  28777  istrkgcb  28778  istrkge  28779  axtgcgrid  28785  axtg5seg  28787  axtgbtwnid  28788  axtgpasch  28789  axtgcont1  28790  axtgeucl  28794  iscgrglt  28836  tgcgr4  28853  axcgrtr  29322  gropd  29438  grstructd  29439  upgredg2vtx  29548  upgredgpr  29549  edglnl  29550  numedglnl  29551  usgredg2vtxeuALT  29632  nbgr2vtx1edg  29760  finsumvtxdg2size  29960  wlkp1lem8  30088  upgrwlkdvdelem  30151  usgr2wlkneq  30171  usgr2pthlem  30178  pthdlem2lem  30182  uspgrn2crct  30226  2pthdlem1  30348  eleclclwwlkn  30496  hashecclwwlkn1  30497  umgrhashecclwwlk  30498  3pthdlem1  30588  eupth2  30663  frgr3vlem1  30697  3vfriswmgrlem  30701  frgrwopreglem4a  30734  frgr2wwlk1  30753  wlkl0  30791  numclwlk2lem2f1o  30803  friendshipgt3  30822  eulplig  30910  nvz  31094  nmobndseqi  31204  nmobndseqiALT  31205  nmlno0  31220  blocnilem  31229  dipdir  31267  dipass  31270  siilem2  31277  ubthlem2  31296  ubth  31298  htth  31343  normpyth  31570  norm3lemt  31577  chlimi  31659  chcompl  31667  omlsii  31828  pjoml  31861  h1de2i  31978  elspansn2  31992  h1datom  32007  pjoml2  32036  pjoml3  32037  lecm  32042  chscllem2  32063  osum  32070  spansncv  32078  pjcjt2  32117  pjopyth  32145  eigre  32260  eigorth  32263  hhcno  32329  hhcnf  32330  cnopc  32338  cnfnc  32355  nmcexi  32451  nmcopexi  32452  nmcfnexi  32476  pjssge0i  32591  hstel2  32644  stj  32660  stri  32682  hstri  32690  stcltr1i  32699  mdbr  32719  mdi  32720  mdbr3  32722  mdbr4  32723  dmdbr  32724  dmdmd  32725  dmdi  32727  dmdbr3  32730  dmdbr4  32731  dmdbr5  32733  mdsl1i  32746  mdslmd1lem3  32752  mdslmd1lem4  32753  mdslmd1i  32754  csmdsymi  32759  cvmd  32761  atss  32771  atom1d  32778  chcv1  32780  hatomic  32785  atord  32813  atcvat2  32814  mddmdin0i  32856  opreu2reuALT  32896  rmoxfrd  32912  ifeqeqx  32961  ssiun2sf  32977  iinabrex  32987  ssrelf  33033  fmptcof2  33075  acunirnmpt  33077  acunirnmpt2  33078  acunirnmpt2f  33079  aciunf1lem  33080  suppovss  33099  fz1nntr  33219  nn0min  33237  fsumiunle  33245  wrdt2ind  33341  ressprs  33352  toslublem  33358  tosglblem  33360  mntoval  33368  ismntd  33370  dfmgc2lem  33381  dfmgc2  33382  xrge0tsmsd  33459  fzto1st  33489  psgnfzto1st  33491  submarchi  33572  archirng  33574  archiexdiv  33576  archiabllem1a  33577  archiabllem2a  33580  archiabl  33584  isarchiofld  33585  gsumvsca1  33612  gsumvsca2  33613  elrgspnlem4  33631  domnpropd  33666  linds2eq  33760  ismxidl  33811  mxidlmax  33814  rprmval  33872  isrprm  33873  rprmdvds  33875  rprmdvdsprod  33890  1arithidomlem1  33891  1arithidom  33893  1arithufdlem3  33902  dfufd2lem  33905  lbsdiflsp0  34082  fedgmullem1  34085  fedgmullem2  34086  fldext2chn  34184  constrmon  34200  submateq  34265  lmatfval  34270  lmatcl  34272  iscref  34300  crefi  34303  pcmplfin  34316  xrge0iifiso  34391  esumcvg  34542  esum2dlem  34548  sigaclcu  34573  sigaclci  34588  unelsiga  34590  unelldsys  34615  sigapildsys  34619  ldgenpisyslem1  34620  fiunelros  34631  measvun  34666  measiun  34675  carsgmon  34771  carsgsigalem  34772  carsgclctunlem2  34776  carsgclctun  34778  pmeasmono  34781  pmeasadd  34782  sibfof  34797  sitgclg  34799  eulerpartlemgvv  34833  signsply0  35005  signstfvneq0  35026  breprexp  35087  hgt749d  35103  istrkg2d  35120  axtgupdim2ALTV  35122  bnj1385  35287  bnj110  35313  bnj222  35338  bnj229  35339  bnj590  35365  bnj865  35378  bnj849  35380  bnj981  35405  bnj1014  35416  bnj1015  35417  bnj1112  35438  bnj1118  35439  bnj1123  35441  bnj1128  35445  bnj1125  35447  bnj1148  35451  bnj1154  35454  bnj1326  35481  bnj1384  35487  bnj1489  35511  bnj1497  35515  r1filimi  35557  trssfir1om  35567  r1omhfb  35568  setindregs  35602  trssfir1omregs  35608  r1omhfbregs  35609  axpowg  35618  onvf1odlem2  35647  cplgredgex  35665  acycgrcycl  35678  subfacp1lem6  35716  erdszelem9  35730  kur14lem9  35745  sconnpht  35760  cvmsss2  35805  cvmliftlem7  35822  cvmliftlem10  35825  fmlasuc  35917  gonar  35926  goalr  35928  mclsrcl  36092  mclsssvlem  36093  mclsval  36094  mclsax  36100  mclsind  36101  mclsppslem  36114  iota5f  36255  fununiq  36300  dfon2lem3  36314  dfon2lem4  36315  dfon2lem5  36316  dfon2lem6  36317  dfon2lem7  36318  dfon2lem8  36319  dfon2  36321  btwnconn1lem11  36628  linethru  36684  fwddifnp1  36696  rankelg  36699  rankeq1o  36702  sbequbidv  36785  cbvralvw2  36797  cbvmodavw  36821  cbvsbdavw  36825  cbvsbdavw2  36826  subtr  36884  subtr2  36885  trer  36886  nn0prpwlem  36892  nn0prpw  36893  neibastop2lem  36930  filnetlem4  36951  axtco1from2  37045  axtcond  37048  axuntco  37049  dfttc4lem2  37099  dfttc4  37100  mh-setindnd  37107  regsfromregtco  37108  regsfromsetind  37109  mh-inf3f1  37111  mh-unprimbi  37114  mh-infprim2bi  37117  bj-hbxfrbi  37294  bj-hbyfrbi  37295  bj-ssblem1  37335  bj-ssblem2  37336  bj-ax12  37338  irrdiff  38029  relowlssretop  38068  rdgeqoa  38075  rdgssun  38083  exrecfnlem  38084  finxpreclem6  38101  pibp19  38119  pibt2  38122  wl-ax12v2cl  38211  wl-mo3t  38290  wl-sb8mot  38294  wl-sb8motv  38295  finixpnum  38315  matunitlindflem1  38326  ptrest  38329  poimirlem13  38343  poimirlem14  38344  poimirlem17  38347  poimirlem18  38348  poimirlem20  38350  poimirlem21  38351  poimirlem22  38352  poimirlem24  38354  poimirlem25  38355  poimirlem26  38356  poimirlem28  38358  poimirlem30  38360  poimirlem31  38361  poimirlem32  38362  poimir  38363  heicant  38365  mblfinlem1  38367  mblfinlem2  38368  mblfinlem3  38369  voliunnfl  38374  volsupnfl  38375  mbfresfi  38376  itg2addnclem3  38383  ftc1cnnc  38402  ftc1anclem7  38409  ftc1anc  38411  findcard4  38424  sdclem2  38453  fdc  38456  fdc1  38457  neificl  38464  mettrifi  38468  sstotbnd2  38485  cntotbnd  38507  heibor1lem  38520  bfp  38535  isass  38557  ismgmOLD  38561  isexid2  38566  iscringd  38709  ispridl  38745  pridl  38748  ismaxidl  38751  maxidlmax  38754  ispridlc  38781  pridlc  38782  dmnnzd  38786  relcnveq2  39038  ecin0  39061  elrelscnveq2  39338  elsymrels3  39347  eltrrels3  39373  eleqvrels3  39386  eqvrelqsel  39409  disjimeceqim2  39514  eldisjim3  39524  eldisjlem19  39622  eldisjsim3  39646  axc11n-16  39772  ax12eq  39775  ax12el  39776  ax12inda  39782  ax12v2-o  39783  fsumshftd  39786  riotasv2d  39791  lshpdisj  39821  lsmsatcv  39844  lsat0cv  39867  lcvexchlem4  39871  lcvexchlem5  39872  l1cvpat  39888  isopos  40014  oposlem  40016  isoml  40072  omllaw  40077  isatl  40133  atlex  40150  iscvlat  40157  cvlexch1  40162  glbconN  40211  hlsuprexch  40215  ps-1  40311  3atlem5  40321  psubspi  40581  llnexchb2  40703  elpcliN  40727  pclfinclN  40784  ldilval  40947  ltrnfset  40951  ltrnset  40952  ltrnu  40955  trlfset  40994  trlset  40995  trlval2  40997  cdleme25cv  41192  cdleme31so  41213  cdleme31fv  41224  cdlemefrs29bpre0  41230  cdleme32fva  41271  cdleme40v  41303  trlord  41403  cdlemkid3N  41767  cdlemkid4  41768  dihffval  42064  dihfval  42065  dihval  42066  lpolconN  42321  mapdordlem2  42471  hdmapfval  42661  hdmapval  42662  hdmapval2  42666  aks4d1p7  42910  isprimroot  42920  primrootlekpowne0  42932  sticksstones1  42973  sticksstones2  42974  sticksstones10  42982  sticksstones12a  42984  aks6d1c6lem3  42999  indstrd  43020  unitscyglem2  43023  unitscyglem3  43024  unitscyglem4  43025  nnn1suc  43093  fsuppind  43382  eu6w  43468  ismrcd1  43489  ismrcd2  43490  ismrc  43492  isnacs3  43501  nacsfix  43503  mzpcompact2  43543  fphpd  43603  fphpdo  43604  monotuz  43728  monotoddzzfi  43729  monotoddzz  43730  oddcomabszz  43731  zindbi  43733  setindtrs  43812  dford3lem2  43814  ttac  43823  dnnumch1  43831  fnwe2lem2  43838  aomclem3  43843  aomclem6  43846  aomclem8  43848  dfac11  43849  dfac21  43853  islssfg2  43858  hbtlem5  43915  hbt  43917  flcidc  43957  mendlmod  43976  unielss  44005  rababg  44360  elmapintrab  44362  iunrelexpuztr  44505  frege92  44741  frege104  44753  ntrkbimka  44824  ntrk0kbimka  44825  neik0pk1imk0  44833  isotone1  44834  isotone2  44835  ntrclsiso  44853  ntrclskb  44855  ntrneiiso  44877  ntrneik3  44882  ntrneix3  44883  gneispacess2  44932  grur1cld  45016  ismnu  45031  mnuop23d  45036  mnuunid  45047  ismnushort  45071  dvgrat  45082  cvgdvgrat  45083  binomcxplemnotnn0  45126  pm14.122b  45193  sbiota1  45204  relprel  45720  relpfrlem  45722  modelaxreplem1  45747  modelaxreplem2  45748  modelaxrep  45750  omssaxinf2  45757  modelac8prim  45761  permaxinf2lem  45781  permac8prim  45783  nregmodel  45786  fnchoice  45809  fiiuncl  45845  iunincfi  45872  disjf1  45961  wessf1ornlem  45963  disjinfi  45970  axccdom  45998  dmrelrnrel  46002  axccd  46004  monoords  46076  fperiodmullem  46082  supxrgere  46109  supxrgelem  46113  supxrge  46114  xrlexaddrp  46128  infxr  46142  infleinf  46147  supxrleubrnmptf  46225  monoordxrv  46255  monoordxr  46256  monoord2xr  46258  fsummulc1f  46347  fsumnncl  46348  fsumf1of  46350  fsumreclf  46352  fsumlessf  46353  fsumsermpt  46355  fmul01  46356  fmulcl  46357  fmuldfeqlem1  46358  fmuldfeq  46359  fmul01lt1lem1  46360  fmul01lt1lem2  46361  fprodexp  46370  fprodabs2  46371  fprodcnlem  46375  climmulf  46380  climexp  46381  climsuse  46384  climrecf  46385  climinff  46387  climaddf  46391  mullimc  46392  mullimcf  46399  limcperiod  46404  sumnnodd  46406  lptre2pt  46414  limsupre  46415  neglimc  46421  addlimc  46422  0ellimcdiv  46423  limclner  46425  climsubmpt  46434  climreclf  46438  climeldmeqmpt  46442  climfveqmpt  46445  fnlimfvre  46448  climfveqf  46454  climfveqmpt3  46456  climeldmeqf  46457  limsupref  46459  limsupbnd1f  46460  climeqf  46462  climeldmeqmpt3  46463  climinf2  46481  limsupubuz  46487  climinf2mpt  46488  climinfmpt  46489  limsupmnf  46495  limsupequz  46497  limsupre2  46499  limsupequzmptf  46505  limsupre3  46507  lmbr3  46521  cnrefiisp  46604  xlimxrre  46605  xlimmnfvlem1  46606  xlimpnfvlem1  46610  climxlim2lem  46619  cncfshift  46648  cncfperiod  46653  icccncfext  46661  fprodcncf  46674  fperdvper  46693  dvmptmulf  46711  dvnmptdivc  46712  dvnmul  46717  dvmptfprod  46719  dvnprodlem1  46720  dvnprodlem2  46721  dvnprodlem3  46722  iblspltprt  46747  itgspltprt  46753  stoweidlem3  46777  stoweidlem4  46778  stoweidlem6  46780  stoweidlem8  46782  stoweidlem15  46789  stoweidlem16  46790  stoweidlem17  46791  stoweidlem19  46793  stoweidlem20  46794  stoweidlem22  46796  stoweidlem23  46797  stoweidlem26  46800  stoweidlem27  46801  stoweidlem30  46804  stoweidlem31  46805  stoweidlem32  46806  stoweidlem34  46808  stoweidlem35  46809  stoweidlem42  46816  stoweidlem43  46817  stoweidlem48  46822  stoweidlem50  46824  stoweidlem51  46825  stoweidlem57  46831  stoweidlem59  46833  stoweidlem62  46836  wallispilem3  46841  dirkercncflem2  46878  fourierdlem11  46892  fourierdlem12  46893  fourierdlem15  46896  fourierdlem16  46897  fourierdlem21  46902  fourierdlem34  46915  fourierdlem41  46922  fourierdlem42  46923  fourierdlem46  46926  fourierdlem48  46928  fourierdlem49  46929  fourierdlem50  46930  fourierdlem51  46931  fourierdlem68  46948  fourierdlem71  46951  fourierdlem72  46952  fourierdlem73  46953  fourierdlem76  46956  fourierdlem79  46959  fourierdlem81  46961  fourierdlem83  46963  fourierdlem86  46966  fourierdlem89  46969  fourierdlem90  46970  fourierdlem91  46971  fourierdlem92  46972  fourierdlem94  46974  fourierdlem97  46977  fourierdlem103  46983  fourierdlem104  46984  fourierdlem111  46991  fourierdlem112  46992  fourierdlem113  46993  etransclem2  47010  etransclem46  47054  salunicl  47090  saluncl  47091  intsaluni  47103  dfsalgen2  47115  sge0f1o  47156  sge0lempt  47184  sge0iunmptlemfi  47187  sge0p1  47188  sge0fodjrnlem  47190  sge0iunmpt  47192  sge0ltfirpmpt2  47200  sge0isummpt2  47206  sge0xaddlem2  47208  sge0xadd  47209  nnfoctbdjlem  47229  meadjuni  47231  meadjiun  47240  voliunsge0lem  47246  meaiuninclem  47254  meaiunincf  47257  meaiuninc3v  47258  meaiuninc3  47259  meaiininclem  47260  meaiininc  47261  omeunile  47279  isomenndlem  47304  ovn0lem  47339  ovnsubaddlem1  47344  hoidmvlelem2  47370  hoidmvlelem3  47371  hoidmvlelem4  47372  hoidmvle  47374  hspmbllem2  47401  hoimbl2  47439  vonhoire  47446  vonicclem2  47458  vonn0ioo2  47464  vonn0icc2  47466  salpreimagelt  47481  salpreimalegt  47483  pimdecfgtioc  47489  pimincfltioc  47490  pimincfltioo  47492  salpreimagtge  47499  salpreimaltle  47500  salpreimagtlt  47504  incsmf  47516  decsmf  47541  smflimlem1  47545  smflimlem2  47546  smflimlem3  47547  smflimlem4  47548  smfpimcclem  47581  funressnmo  47843  fcoresf1  47866  aiota0def  47893  euoreqb  47906  2reu8i  47910  2reuimp0  47911  funressndmafv2rn  48020  funressnbrafv2  48041  funbrafv2  48044  smonoord  48174  elsetpreimafvbi  48200  iccpartgt  48236  iccelpart  48242  iccpartiun  48243  icceuelpartlem  48244  icceuelpart  48245  iccpartnel  48247  fargshiftf1  48250  ichexmpl2  48279  ichnreuop  48281  ichreuopeq  48282  sprsymrelfolem2  48302  prproropf1olem4  48315  paireqne  48320  reupr  48331  reuopreuprim  48335  fmtnofac2  48381  fmtnofac1  48382  prmdvdsfmtnof1lem2  48397  perfectALTVlem2  48547  nfermltl8rev  48567  nfermltl2rev  48568  sbgoldbwt  48602  sbgoldbst  48603  sgoldbeven3prm  48608  sbgoldbm  48609  nnsum4primesodd  48621  nnsum4primesoddALTV  48622  evengpop3  48623  evengpoap3  48624  bgoldbnnsum3prm  48629  bgoldbtbndlem4  48633  bgoldbtbnd  48634  tgblthelfgott  48640  tgoldbach  48642  grimuhgr  48712  grimcnv  48713  isuspgrimlem  48720  isubgr3stgrlem4  48794  isubgr3stgrlem6  48796  isubgr3stgrlem7  48797  gpgedg2ov  48891  gpgedg2iv  48892  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  pgnbgreunbgrlem2lem3  48941  pgnbgreunbgrlem5lem1  48945  pgnbgreunbgrlem5lem2  48946  pgnbgreunbgrlem5lem3  48947  pgnbgreunbgr  48950  idomnzd  49170  ply1mulgsumlem2  49226  islininds  49285  linindslinci  49287  lindslinindsimp1  49296  linds0  49304  lindsrng01  49307  snlindsntorlem  49309  snlindsntor  49310  ldepsnlinc  49347  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  nn0sumshdiglem1  49460  nn0sumshdiglem2  49461  nn0sumshdig  49462  itschlc0yqe  49599  f1mo  49690  iscnrm3lem5  49774  iscnrm3r  49785  isprsd  49792  lubeldm2d  49795  glbeldm2d  49796  joindm2  49805  meetdm2  49807  ipolublem  49823  ipolub  49825  ipoglblem  49826  ipoglb  49828  oppcendc  49855  oppcthinendcALT  50278  functhinclem2  50282  fullthinc  50287  fullthinc2  50288  euendfunc  50363  bnd2d  50518  setrec1lem1  50524  setrec1lem4  50527  setrec2fun  50529  alsbid  50639  cbvals  50642