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  2261  cbvsbvf  2393  drnf1v  2401  drnf1  2473  mo4  2592  cbvmovw  2628  cbvmow  2629  axextg  2735  rspw  3240  cbvralvw  3241  cbvralfw  3303  raleqbidv  3335  cbvraldva2  3337  sbralie  3339  sbralieOLD  3341  cbvralf  3346  ralcom2  3363  vtoclgaf  3536  vtoclga  3537  rspct  3563  rspc  3565  rspc2gv  3586  rexraleqim  3601  ralab2  3655  nelrdva  3663  mob2  3673  mob  3675  morex  3677  reu7  3690  reu8  3691  reu2eqd  3694  cdeqim  3731  sbcimg  3787  sbcim1  3792  sbceqal  3800  csbhypf  3875  cbvralcsf  3889  dfssf  3922  reldisj  4406  ralidmw  4472  reusngf  4635  rexreusng  4640  reuprg0  4663  elpreqpr  4827  unissb  4901  intss1  4923  intmin  4928  dftr2c  5215  trel  5220  zfpow  5328  reusv2lem4  5363  reusv3i  5366  rext  5416  opth  5445  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  poeq1  5562  pocl  5567  swopolem  5569  swopo  5570  isso2i  5596  vtoclr  5714  poinxp  5732  posn  5737  ssrel  5759  ssrel2  5761  ssrelrel  5772  relop  5828  cotrg  6105  cnvsym  6108  reu3op  6295  reuop  6296  dfpo2  6299  preddowncl  6335  frpoinsg  6346  ordelord  6384  iota5  6521  dffun2  6548  fununiq  6555  sbcfungOLD  6564  funopg  6574  brprcneu  6875  brprcneuALT  6876  tz6.12f  6910  funbrfv  6933  ssimaexg  6971  fvmptf  7015  fvelrn  7076  fprg  7159  dff13f  7259  f1veqaeq  7260  fpropnf1  7271  f1ounsn  7280  nf1const  7312  soisores  7335  soisoi  7336  isofrlem  7348  isopolem  7353  weniso  7364  riota5f  7405  imbrov2fvoveq  7445  oprabidw  7451  oprabid  7452  f1opr  7476  ovmpos  7568  ov2gf  7569  ov3  7583  caovcan  7625  caovordig  7626  caofrss  7732  caoftrn  7734  tfisg  7865  tfis  7866  tfisi  7870  tfindsg  7872  tfindsg2  7873  tfindes  7874  dfom2  7879  limomss  7882  nnlim  7891  peano5  7905  findsg  7909  findes  7912  resf1extb  7946  f1oweALT  7984  dfoprab4f  8067  offval22  8099  f1o2ndf1  8133  frxp  8138  poxp  8140  fnwe2lem3  8147  frpoins3xpg  8157  frpoins3xp3g  8158  poxp2  8160  frxp2  8161  xpord2indlem  8164  poxp3  8167  frxp3  8168  xpord3inddlem  8171  suppfnss  8206  onfununi  8349  smoel  8368  smogt  8375  tfrlem1  8383  onelfvnef1  8449  tz7.48lemOLD  8451  tz7.49  8455  oawordeu  8563  omordi  8574  oeordi  8596  nnmordi  8640  omabs  8660  nneob  8665  omsmolem  8666  qsel  8817  eroveu  8833  ecopovtrn  8841  ixpsnf1o  8966  funen1cnv  9056  fundmeng  9060  sbth  9116  limensuc  9173  findcard  9179  findcard2  9180  findcard2d  9182  pssnn  9184  ssfi  9188  sbthfi  9214  nneneq  9221  php  9222  unxpdom  9250  findcard3  9274  ac6sfi  9275  frfi  9276  domunfican  9313  fiint  9318  iunfi  9332  finsschain  9348  dffi3  9423  marypha1lem  9425  marypha1  9426  supeq3  9441  supeq123d  9442  supmo  9444  suplub  9452  supisolem  9466  eqinf  9477  infval  9479  infmo  9489  ordiso2  9509  ordtypelem7  9518  wemaplem1  9540  wemaplem2  9541  zfregcl  9588  zfregclOLD  9589  elirrv  9591  elirrvOLD  9592  inf0  9622  inf3lem1  9629  zfinf  9640  axinf2  9641  dfom3  9648  elom3  9649  cantnfval2  9670  cantnfle  9672  cantnflt  9673  cantnfp1lem3  9681  oemapvali  9685  cantnflem1c  9688  cantnflem1  9690  cantnf  9694  wemapwe  9698  cnfcom  9701  ttrclss  9721  ttrclselem2  9727  setind  9748  setinds  9750  frmin  9753  frinsg  9755  r1sdom  9781  r1ordg  9785  rankonidlem  9838  rankelg  9852  rankunb  9864  r1filimi  9903  scottabf  9939  bnd2  9956  setrec1lem1  9966  bnd2d  9968  setrec1lem4  9971  setrec2fun  9973  infxpenlem  10092  infxpenc2  10101  dfac8alem  10108  dfac8clem  10111  indcardi  10120  alephordi  10153  alephinit  10174  alephfp  10187  aceq3lem  10199  dfac5lem4  10205  dfac5  10207  dfac2b  10209  dfac9  10215  dfac12lem2  10223  dfac12lem3  10224  kmlem1  10229  kmlem4  10232  kmlem10  10238  kmlem12  10240  kmlem13  10241  pwsdompw  10281  ackbij1lem16  10312  cfslb2n  10346  cfsmolem  10348  sornom  10355  fin2i  10373  infpssrlem4  10384  isfin2-2  10397  isfin3ds  10407  fin23lem17  10416  fin23lem32  10422  fin23lem34  10424  fin23lem35  10425  fin23lem39  10428  fin23lem41  10430  isf32lem2  10432  isf33lem  10444  isf34lem4  10455  isf34lem6  10458  fin1a2lem10  10487  axcc2lem  10514  axcc3  10516  axcc4dom  10519  dominf  10523  axdc2lem  10526  axdc3lem2  10529  ac6sg  10566  zorn2lem7  10580  zornn0g  10583  ttukeylem5  10591  ttukeylem6  10592  axdclem  10597  dominfac  10658  axrepndlem1  10677  axrepndlem2  10678  axunndlem1  10680  axunnd  10681  axpowndlem2  10683  axpowndlem3  10684  axpowndlem4  10685  axregndlem2  10688  axregnd  10689  axinfndlem1  10690  axinfnd  10691  axacndlem4  10695  axacndlem5  10696  axacnd  10697  zfcndpow  10701  zfcndinf  10703  fpwwe2lem4  10719  fpwwe2lem7  10722  fpwwe2lem11  10726  pwfseqlem4a  10746  pwfseqlem4  10747  pwfseqlem5  10748  pwfseq  10749  wunfi  10806  wunex2  10823  inar1  10860  rankcf  10862  tskord  10865  grudomon  10902  grur1a  10904  axgroth6  10913  axgroth3  10916  axgroth4  10917  eltskm  10928  indpi  10992  pinq  11012  nqereu  11014  prcdnq  11078  prnmax  11080  ltsopr  11117  prlem936  11132  ltsosr  11179  recexsrlem  11188  mulgt0sr  11190  map2psrpr  11195  supsrlem  11196  axrrecex  11248  axpre-lttrn  11251  axpre-mulgt0  11253  axpre-sup  11254  axsup  11385  dedekind  11473  ltordlem  11841  ltord1  11842  wloglei  11848  squeeze0  12220  infm3  12276  nnsub  12382  nnunb  12602  peano5uzti  12789  fzind  12797  uzind4s  13035  uzind4s2  13036  zmax  13072  zbtwnre  13073  xmulasslem  13415  xrsupsslem  13437  xrinfmsslem  13438  xrub  13442  infmremnf  13474  injresinj  13926  f1resfz0f1d  13927  om2uzlti  14093  uzindi  14125  axdc4uz  14127  ssnn0fi  14128  rabssnn0fi  14129  suppssfz  14137  seqp1  14159  seqcl2  14163  seqfveq2  14167  seqshft2  14171  monoord  14175  seqsplit  14178  seqf1olem2  14185  seqf1o  14186  seqid2  14191  seqhomo  14192  seqof2  14203  expcl2lem  14216  facdiv  14431  facwordi  14433  faclbnd4lem2  14438  hashnn0n0nn  14535  hashf1lem2  14601  seqcoll  14609  fi1uzind  14652  brfi1indALT  14655  wrdind  14871  wrd2ind  14872  swrdccatin1  14874  swrdccat3blem  14888  reuccatpfxs1lem  14895  repswccat  14937  cshf1  14961  trclfvcotr  15162  relexprelg  15191  rtrclreclem4  15214  relexpindlem  15216  ello1mpt  15688  o1co  15753  o1compt  15754  rlimcn3  15757  climcn2  15760  subcn2  15762  o1of2  15780  fsumclf  15904  fsumsplitf  15908  fsumsplit1  15911  fsum2d  15937  modfsummod  15961  fsumabs  15968  telfsumo  15969  fsumrlim  15978  fsumo1  15979  o1fsum  15980  fsumiun  15988  prodfdiv  16065  fprod2d  16148  fproddivf  16154  fprodsplitf  16155  fprodsplit1f  16157  rpnnen2lem10  16391  sqrt2irr  16417  dvdsle  16480  divalglem7  16569  divalglem8  16570  ndvdssub  16579  gcdcllem1  16669  dfgcd2  16719  algcvg  16751  algcvga  16754  algfx  16755  lcmgcdlem  16781  lcmdvds  16783  lcmf  16808  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem  16816  lcmfdvds  16817  lcmfun  16820  coprmgcdb  16824  coprmdvds1  16827  coprmdvds2  16829  coprmprod  16836  coprmproddvds  16838  prmind2  16860  dvdsprime  16862  nprm  16863  dvdsprm  16879  exprmfct  16880  coprm  16887  isprm6  16890  prmfac1  16896  eulerthlem2  16959  pcqmul  17031  pcqcl  17034  pc2dvds  17057  pcz  17059  prmpwdvds  17082  infpn2  17091  vdwlem12  17170  ramub2  17192  rami  17193  ramcl  17207  prmdvdsprmop  17221  prmlem0  17283  mreintcl  17765  ismred2  17773  mrissmrcd  17814  mreexexlemd  17818  iscatd2  17855  moni  17911  yoniso  18459  isprs  18470  prslem  18471  drsdirfi  18479  ispos  18488  posi  18491  isposd  18496  pospropd  18499  lubfval  18522  lublecllem  18532  glbfval  18535  joinle  18558  meetle  18572  poslubmo  18583  posglbmo  18584  resspos  18603  lubl  18686  lubun  18689  clatleglb  18692  ipodrsima  18715  acsdrsel  18717  isacs4lem  18718  isacs5lem  18719  acsdrscl  18720  mreclatBAD  18737  pslem  18746  dirtr  18776  chnind  18795  mndind  19024  degenmgm2nfun  19139  mhmlem  19272  isnsg2  19366  ghmf1  19460  orbsta  19527  symgextf1  19635  gsmsymgrfix  19642  gsmsymgreq  19646  symggen  19684  psgnunilem4  19711  sylow1lem1  19812  sylow2alem2  19832  sylow2a  19833  lsmmod  19889  lsmdisj2  19896  efgsrel  19948  efgredlemd  19958  efgredlem  19961  efgred  19962  gsumzaddlem  20135  gsummptnn0fz  20200  gsummptnn0fzfv  20201  telgsumfzs  20203  telgsums  20207  dprdval  20219  dprddisj2  20255  ablfac1eulem  20288  pgpfac1lem1  20290  pgpfac1lem5  20295  pgpfac1  20296  pgpfaclem2  20298  pgpfac  20300  isomnd  20337  omndadd  20342  gsumle  20359  irredmul  20659  islring  20792  lringuplu  20796  rrgval  20949  rrgeq0i  20951  isdomn  20957  domneq0  20960  isdomn4  20967  domnlcanb  20971  domnrcanb  20973  isdrngrd  21023  isdrngrdOLD  21025  sdrgacs  21058  isorng  21118  orngmul  21122  islbs3  21433  rngqiprngimf1lem  21590  isprmidl  21619  prmidl  21621  prmidlc  21629  prmidlprop  21632  ssdifidlprm  21642  cnsubrglem  21723  prmirredlem  21778  znfld  21866  znrrg  21871  cygznlem3  21875  isphl  21934  ipeq0  21944  isphld  21960  phlpropd  21961  lsmcss  21998  frlmphl  22087  frlmup1  22104  lindfrn  22127  islindf4  22144  islindf5  22145  mplsubglem  22306  mpllsslem  22307  mplcoe1  22346  mplcoe5  22349  mpfind  22424  ismhp3  22463  coe1fzgsumd  22622  gsummoncoe1  22626  pf1ind  22673  evl1gsumd  22675  dmatelnd  22811  mat1scmat  22854  mdetdiaglem  22913  mdetralt  22923  mdetralt2  22924  mdetunilem1  22927  mdetunilem2  22928  mdetunilem3  22929  mdetunilem4  22930  mdetunilem9  22935  smadiadetr  22990  matunitlindflem1  22994  pmatcoe1fsupp  23019  mp2pm2mplem4  23127  uniopn  23215  fiinopn  23219  epttop  23327  clsndisj  23393  elcls3  23401  neiptoptop  23449  neiptopnei  23450  cnpval  23554  iscnp  23555  cnpimaex  23574  lmcvg  23580  cnprest  23607  cnprest2  23608  lmss  23616  lmff  23619  t0sep  23642  hausnei  23646  isnrm2  23676  t1sep2  23687  isreg2  23695  iscmp  23706  cmpcov  23707  cmpsublem  23717  cmpsub  23718  tgcmp  23719  uncmp  23721  fiuncmp  23722  hauscmplem  23724  cmpfi  23726  cmpfii  23727  dfconn2  23737  connsuba  23738  connsub  23739  nconnsubb  23741  1stcclb  23762  1stcfb  23763  2ndc1stc  23769  1stcrest  23771  1stcelcls  23780  restnlly  23801  lly1stc  23815  comppfsc  23851  kgenval  23854  kgeni  23856  kgencn2  23876  ptcldmpt  23933  ptclsg  23934  dfac14lem  23936  dfac14  23937  txcnp  23939  ptcnp  23941  hausdiag  23964  txlm  23967  tx1stc  23969  xkococn  23979  cnmpt12  23986  cnmpt22  23993  kqt0lem  24055  isr0  24056  regr1lem2  24059  kqreglem1  24060  r0sep  24067  ptcmpfi  24132  elmptrab  24146  isfil  24166  filss  24172  isufil2  24227  cfinufil  24247  rnelfm  24272  fmfnfmlem2  24274  fmfnfmlem4  24276  flimopn  24294  flimrest  24302  flftg  24315  cnpflf  24320  txflf  24325  fclsopni  24334  fclsrest  24343  fclscf  24344  flimfnfcls  24347  fcfnei  24354  alexsublem  24363  alexsubb  24365  alexsubALTlem3  24368  alexsubALTlem4  24369  alexsubALT  24370  cnextcn  24386  cnextfres1  24387  tgpt0  24438  qustgplem  24440  tsmsi  24453  tsmssubm  24462  tsmsres  24463  tsmsf1o  24464  tsmsxp  24474  ustssel  24525  ust0  24539  ustuqtop4  24563  ucnima  24599  ucncn  24603  iscusp  24617  cuspcvg  24619  imasdsf1olem  24692  blssps  24743  blss  24744  metss  24827  comet  24832  metcnp3  24859  metcnp2  24861  txmetcnp  24866  metuel2  24884  metucn  24890  nrmmetd  24893  nlmvscn  25006  nrginvrcn  25011  nmolb  25036  xrge0tsms  25154  mpomulcn  25188  divcn  25189  fsumcn  25191  elcncf2  25211  cncfi  25215  mulc1cncf  25226  cncfmet  25230  xrhmeo  25267  bndth  25279  nmoleub2lem2  25437  nmoleub3  25440  ipcn  25567  lmmbr  25579  caucfil  25604  pmltpc  25771  ovolfiniun  25822  ovolicc2lem3  25840  ovolicc2  25843  mblsplit  25853  finiunmbl  25865  volfiniun  25868  voliunlem3  25873  ioorinv  25897  ioorcl  25898  dyadmax  25919  dyadmbllem  25920  dyadmbl  25921  opnmbllem  25922  volcn  25927  vitalilem2  25930  vitalilem3  25931  vitali  25934  i1fd  26002  itg2seq  26063  itg2addlem  26079  itgfsum  26147  ellimc3  26199  dvbsss  26222  dvnres  26251  dvmptfsum  26295  dvferm1lem  26304  dvferm2lem  26306  rolle  26310  c1lip1  26317  lhop1lem  26333  lhop1  26334  dvfsumlem2  26347  dvfsumlem4  26349  dvfsumrlim  26351  dvfsum2  26354  ftc1a  26357  ftc1lem6  26361  mdegleb  26382  mdeglt  26383  deg1leb  26413  deg1lt  26415  ply1divex  26455  fta1glem2  26487  fta1g  26488  plyco0  26510  plyeq0lem  26529  coeeq2  26561  dgrle  26562  dgrcolem2  26593  dgrco  26594  plydivlem4  26617  plydivex  26618  fta1lem  26628  fta1  26629  vieta1lem2  26634  vieta1  26635  aalioulem2  26660  aalioulem4  26662  abelth  26768  cxpcn3  27076  rlimcnp  27293  xrlimcnp  27296  cxploglim  27305  scvxcvx  27313  jensen  27316  lgamgulmlem2  27357  wilthlem2  27396  wilthlem3  27397  fta  27407  mpodvdsmulf1o  27521  dvdsmulf1o  27523  perfectlem2  27557  dchrelbas3  27565  dchrelbas4  27570  dchrn0  27577  bcmono  27604  lgsdir2lem4  27655  lgsdchr  27682  gausslemma2dlem0i  27691  lgseisenlem2  27703  lgsquad2lem2  27712  2sqlem6  27750  2sqlem8  27753  2sqlem10  27755  dchrisumlema  27815  dchrisumlem2  27817  dchrisumlem3  27818  fltoprmlem2  27994  fltoprm  27995  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupdm  28061  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem3  28067  nosupbnd1lem5  28069  nosupbnd2  28073  noinfcbv  28074  noinfdm  28076  noinffv  28078  noinfres  28079  noinfbnd1lem1  28080  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noinfbnd2  28088  nocvxminlem  28140  madebdaylemold  28284  madebdaylemlrcut  28285  madebday  28286  lrrecpo  28327  addsproplem1  28355  addsprop  28362  leadds1  28375  negsproplem1  28414  negsprop  28421  mulsproplemcbv  28501  mulsproplem1  28502  mulsprop  28516  precsexlem8  28600  precsexlem9  28601  precsexlem11  28603  precsex  28604  bdayons  28662  addonbday  28665  onsfi  28742  n0subs  28749  oldfib  28763  eln0zs  28786  bdaypw2n0bndlem  28849  bdaypw2n0bnd  28850  bdayfinbndcbv  28852  bdayfinbndlem1  28853  bdayfinbndlem2  28854  bdayfinbnd  28855  istrkgb  28917  istrkgcb  28918  istrkge  28919  axtgcgrid  28925  axtg5seg  28927  axtgbtwnid  28928  axtgpasch  28929  axtgcont1  28930  axtgeucl  28934  iscgrglt  28977  tgcgr4  28994  axcgrtr  29493  gropd  29609  grstructd  29610  upgredg2vtx  29719  upgredgpr  29720  edglnl  29721  numedglnl  29722  usgredg2vtxeuALT  29803  nbgr2vtx1edg  29931  finsumvtxdg2size  30131  wlkp1lem8  30259  upgrwlkdvdelem  30322  usgr2wlkneq  30342  usgr2pthlem  30349  pthdlem2lem  30353  uspgrn2crct  30397  2pthdlem1  30519  eleclclwwlkn  30667  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  acycgrcycl  30753  3pthdlem1  30765  eupth2  30840  frgr3vlem1  30874  3vfriswmgrlem  30878  frgrwopreglem4a  30911  frgr2wwlk1  30930  wlkl0  30968  numclwlk2lem2f1o  30980  friendshipgt3  30999  eulplig  31087  nvz  31271  nmobndseqi  31381  nmobndseqiALT  31382  nmlno0  31397  blocnilem  31406  dipdir  31444  dipass  31447  siilem2  31454  ubthlem2  31473  ubth  31475  htth  31520  normpyth  31747  norm3lemt  31754  chlimi  31836  chcompl  31844  omlsii  32005  pjoml  32038  h1de2i  32155  elspansn2  32169  h1datom  32184  pjoml2  32213  pjoml3  32214  lecm  32219  chscllem2  32240  osum  32247  spansncv  32255  pjcjt2  32294  pjopyth  32322  eigre  32437  eigorth  32440  hhcno  32506  hhcnf  32507  cnopc  32515  cnfnc  32532  nmcexi  32628  nmcopexi  32629  nmcfnexi  32653  pjssge0i  32768  hstel2  32821  stj  32837  stri  32859  hstri  32867  stcltr1i  32876  mdbr  32896  mdi  32897  mdbr3  32899  mdbr4  32900  dmdbr  32901  dmdmd  32902  dmdi  32904  dmdbr3  32907  dmdbr4  32908  dmdbr5  32910  mdsl1i  32923  mdslmd1lem3  32929  mdslmd1lem4  32930  mdslmd1i  32931  csmdsymi  32936  cvmd  32938  atss  32948  atom1d  32955  chcv1  32957  hatomic  32962  atord  32990  atcvat2  32991  mddmdin0i  33033  opreu2reuALT  33073  rmoxfrd  33089  ifeqeqx  33138  ssiun2sf  33154  iinabrex  33163  ssrelf  33209  fmptcof2  33251  acunirnmpt  33253  acunirnmpt2  33254  acunirnmpt2f  33255  aciunf1lem  33256  suppovss  33274  fz1nntr  33394  nn0min  33412  fsumiunle  33420  wrdt2ind  33516  ressprs  33527  toslublem  33533  tosglblem  33535  mntoval  33543  ismntd  33545  dfmgc2lem  33556  dfmgc2  33557  xrge0tsmsd  33634  fzto1st  33664  psgnfzto1st  33666  submarchi  33747  archirng  33749  archiexdiv  33751  archiabllem1a  33752  archiabllem2a  33755  archiabl  33759  isarchiofld  33760  gsumvsca1  33787  gsumvsca2  33788  elrgspnlem4  33806  domnpropd  33841  linds2eq  33936  ismxidl  33987  mxidlmax  33990  rprmval  34048  isrprm  34049  rprmdvds  34051  rprmdvdsprod  34066  1arithidomlem1  34067  1arithidom  34069  1arithufdlem3  34078  dfufd2lem  34081  lbsdiflsp0  34258  fedgmullem1  34261  fedgmullem2  34262  fldext2chn  34360  constrmon  34376  submateq  34441  lmatfval  34446  lmatcl  34448  iscref  34476  crefi  34479  pcmplfin  34492  xrge0iifiso  34567  esumcvg  34718  esum2dlem  34724  sigaclcu  34749  sigaclci  34764  unelsiga  34766  unelldsys  34791  sigapildsys  34795  ldgenpisyslem1  34796  fiunelros  34807  measvun  34842  measiun  34851  carsgmon  34946  carsgsigalem  34947  carsgclctunlem2  34951  carsgclctun  34953  pmeasmono  34956  pmeasadd  34957  sibfof  34972  sitgclg  34974  eulerpartlemgvv  35008  signsply0  35180  signstfvneq0  35201  breprexp  35262  hgt749d  35278  istrkg2d  35295  axtgupdim2ALTV  35297  bnj1385  35462  bnj110  35488  bnj222  35513  bnj229  35514  bnj590  35540  bnj865  35553  bnj849  35555  bnj981  35580  bnj1014  35591  bnj1015  35592  bnj1112  35613  bnj1118  35614  bnj1123  35616  bnj1128  35620  bnj1125  35622  bnj1148  35626  bnj1154  35629  bnj1326  35656  bnj1384  35662  bnj1489  35686  bnj1497  35690  trssfir1om  35737  r1omhfb  35738  setindregs  35798  trssfir1omregs  35804  r1omhfbregs  35805  axpowg  35814  onvf1odlem2  35883  cplgredgex  35905  subfacp1lem6  35950  erdszelem9  35964  kur14lem9  35979  sconnpht  35994  cvmsss2  36039  cvmliftlem7  36056  cvmliftlem10  36059  fmlasuc  36151  gonar  36160  goalr  36162  mclsrcl  36326  mclsssvlem  36327  mclsval  36328  mclsax  36334  mclsind  36335  mclsppslem  36348  iota5f  36489  dfon2lem3  36547  dfon2lem4  36548  dfon2lem5  36549  dfon2lem6  36550  dfon2lem7  36551  dfon2lem8  36552  dfon2  36554  btwnconn1lem11  36862  linethru  36918  fwddifnp1  36930  rankeq1o  36932  sbequbidv  37003  cbvralvw2  37015  cbvmodavw  37039  cbvsbdavw  37043  cbvsbdavw2  37044  subtr  37102  subtr2  37103  trer  37104  nn0prpwlem  37110  nn0prpw  37111  neibastop2lem  37148  filnetlem4  37169  axtco1from2  37263  axtcond  37266  axuntco  37267  dfttc4lem2  37317  dfttc4  37318  mh-setindnd  37325  regsfromregtco  37326  regsfromsetind  37327  mh-unprimbi  37332  mh-infprim2bi  37335  bj-hbxfrbi  37512  bj-hbyfrbi  37513  bj-ssblem1  37553  bj-ssblem2  37554  bj-ax12  37556  irrdiff  38247  relowlssretop  38286  rdgeqoa  38293  rdgssun  38301  exrecfnlem  38302  finxpreclem6  38319  pibp19  38337  pibt2  38340  wl-ax12v2cl  38429  wl-mo3t  38508  wl-sb8mot  38512  wl-sb8motv  38513  finixpnum  38528  ptrest  38537  poimirlem13  38551  poimirlem14  38552  poimirlem17  38555  poimirlem18  38556  poimirlem20  38558  poimirlem21  38559  poimirlem22  38560  poimirlem24  38562  poimirlem25  38563  poimirlem26  38564  poimirlem28  38566  poimirlem30  38568  poimirlem31  38569  poimirlem32  38570  poimir  38571  heicant  38573  mblfinlem1  38575  mblfinlem2  38576  mblfinlem3  38577  voliunnfl  38582  volsupnfl  38583  mbfresfi  38584  itg2addnclem3  38591  ftc1cnnc  38610  ftc1anclem7  38617  ftc1anc  38619  findcard4  38632  sdclem2  38676  fdc  38679  fdc1  38680  neificl  38687  mettrifi  38691  sstotbnd2  38708  cntotbnd  38730  heibor1lem  38743  bfp  38758  isass  38780  ismgmOLD  38784  isexid2  38789  iscringd  38932  ispridl  38968  pridl  38971  ismaxidl  38974  maxidlmax  38977  ispridlc  39004  pridlc  39005  dmnnzd  39009  relcnveq2  39261  ecin0  39284  elrelscnveq2  39561  elsymrels3  39570  eltrrels3  39596  eleqvrels3  39609  eqvrelqsel  39632  disjimeceqim2  39737  eldisjim3  39747  eldisjlem19  39845  eldisjsim3  39869  axc11n-16  39995  ax12eq  39998  ax12el  39999  ax12inda  40005  ax12v2-o  40006  fsumshftd  40009  riotasv2d  40014  lshpdisj  40044  lsmsatcv  40067  lsat0cv  40090  lcvexchlem4  40094  lcvexchlem5  40095  l1cvpat  40111  isopos  40237  oposlem  40239  isoml  40295  omllaw  40300  isatl  40356  atlex  40373  iscvlat  40380  cvlexch1  40385  glbconN  40434  hlsuprexch  40438  ps-1  40534  3atlem5  40544  psubspi  40804  llnexchb2  40926  elpcliN  40950  pclfinclN  41007  ldilval  41170  ltrnfset  41174  ltrnset  41175  ltrnu  41178  trlfset  41217  trlset  41218  trlval2  41220  cdleme25cv  41415  cdleme31so  41436  cdleme31fv  41447  cdlemefrs29bpre0  41453  cdleme32fva  41494  cdleme40v  41526  trlord  41626  cdlemkid3N  41990  cdlemkid4  41991  dihffval  42287  dihfval  42288  dihval  42289  lpolconN  42544  mapdordlem2  42694  hdmapfval  42884  hdmapval  42885  hdmapval2  42889  aks4d1p7  43133  isprimroot  43143  primrootlekpowne0  43155  sticksstones1  43196  sticksstones2  43197  sticksstones10  43205  sticksstones12a  43207  aks6d1c6lem3  43222  indstrd  43243  unitscyglem2  43246  unitscyglem3  43247  unitscyglem4  43248  nnn1suc  43331  fsuppind  43618  eu6w  43687  ismrcd1  43708  ismrcd2  43709  ismrc  43711  isnacs3  43720  nacsfix  43722  mzpcompact2  43762  fphpd  43822  fphpdo  43823  monotuz  43947  monotoddzzfi  43948  monotoddzz  43949  oddcomabszz  43950  zindbi  43952  setindtrs  44031  dford3lem2  44033  ttac  44042  dnnumch1  44050  aomclem3  44057  aomclem6  44060  aomclem8  44062  dfac11  44063  dfac21  44067  islssfg2  44072  hbtlem5  44129  hbt  44131  flcidc  44171  mendlmod  44190  unielss  44219  rababg  44574  elmapintrab  44576  iunrelexpuztr  44718  frege92  44954  frege104  44966  ntrkbimka  45037  ntrk0kbimka  45038  neik0pk1imk0  45046  isotone1  45047  isotone2  45048  ntrclsiso  45066  ntrclskb  45068  ntrneiiso  45090  ntrneik3  45095  ntrneix3  45096  gneispacess2  45145  grur1cld  45229  ismnu  45244  mnuop23d  45249  mnuunid  45260  ismnushort  45284  dvgrat  45295  cvgdvgrat  45296  binomcxplemnotnn0  45339  pm14.122b  45406  sbiota1  45417  relprel  45940  relpfrlem  45942  modelaxreplem1  45967  modelaxreplem2  45968  modelaxrep  45970  omssaxinf2  45977  modelac8prim  45981  permaxinf2lem  46001  permac8prim  46003  nregmodel  46006  fnchoice  46045  fiiuncl  46081  iunincfi  46108  disjf1  46197  wessf1ornlem  46199  disjinfi  46206  axccdom  46234  dmrelrnrel  46238  axccd  46240  monoords  46312  fperiodmullem  46318  supxrgere  46344  supxrgelem  46348  supxrge  46349  xrlexaddrp  46363  infxr  46377  infleinf  46382  supxrleubrnmptf  46460  monoordxrv  46490  monoordxr  46491  monoord2xr  46493  fsummulc1f  46582  fsumnncl  46583  fsumf1of  46585  fsumreclf  46587  fsumlessf  46588  fsumsermpt  46590  fmul01  46591  fmulcl  46592  fmuldfeqlem1  46593  fmuldfeq  46594  fmul01lt1lem1  46595  fmul01lt1lem2  46596  fprodexp  46605  fprodabs2  46606  fprodcnlem  46610  climmulf  46615  climexp  46616  climsuse  46619  climrecf  46620  climinff  46622  climaddf  46626  mullimc  46627  mullimcf  46634  limcperiod  46639  sumnnodd  46641  lptre2pt  46649  limsupre  46650  neglimc  46656  addlimc  46657  0ellimcdiv  46658  limclner  46660  climsubmpt  46669  climreclf  46673  climeldmeqmpt  46677  climfveqmpt  46680  fnlimfvre  46683  climfveqf  46689  climfveqmpt3  46691  climeldmeqf  46692  limsupref  46694  limsupbnd1f  46695  climeqf  46697  climeldmeqmpt3  46698  climinf2  46716  limsupubuz  46722  climinf2mpt  46723  climinfmpt  46724  limsupmnf  46730  limsupequz  46732  limsupre2  46734  limsupequzmptf  46740  limsupre3  46742  lmbr3  46756  cnrefiisp  46839  xlimxrre  46840  xlimmnfvlem1  46841  xlimpnfvlem1  46845  climxlim2lem  46854  cncfshift  46883  cncfperiod  46888  icccncfext  46896  fprodcncf  46909  fperdvper  46928  dvmptmulf  46946  dvnmptdivc  46947  dvnmul  46952  dvmptfprod  46954  dvnprodlem1  46955  dvnprodlem2  46956  dvnprodlem3  46957  iblspltprt  46982  itgspltprt  46988  stoweidlem3  47012  stoweidlem4  47013  stoweidlem6  47015  stoweidlem8  47017  stoweidlem15  47024  stoweidlem16  47025  stoweidlem17  47026  stoweidlem19  47028  stoweidlem20  47029  stoweidlem22  47031  stoweidlem23  47032  stoweidlem26  47035  stoweidlem27  47036  stoweidlem30  47039  stoweidlem31  47040  stoweidlem32  47041  stoweidlem34  47043  stoweidlem35  47044  stoweidlem42  47051  stoweidlem43  47052  stoweidlem48  47057  stoweidlem50  47059  stoweidlem51  47060  stoweidlem57  47066  stoweidlem59  47068  stoweidlem62  47071  wallispilem3  47076  dirkercncflem2  47113  fourierdlem11  47127  fourierdlem12  47128  fourierdlem15  47131  fourierdlem16  47132  fourierdlem21  47137  fourierdlem34  47150  fourierdlem41  47157  fourierdlem42  47158  fourierdlem46  47161  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem51  47166  fourierdlem68  47183  fourierdlem71  47186  fourierdlem72  47187  fourierdlem73  47188  fourierdlem76  47191  fourierdlem79  47194  fourierdlem81  47196  fourierdlem83  47198  fourierdlem86  47201  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem92  47207  fourierdlem94  47209  fourierdlem97  47212  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  fourierdlem112  47227  fourierdlem113  47228  etransclem2  47245  etransclem46  47289  salunicl  47325  saluncl  47326  intsaluni  47338  dfsalgen2  47350  sge0f1o  47391  sge0lempt  47419  sge0iunmptlemfi  47422  sge0p1  47423  sge0fodjrnlem  47425  sge0iunmpt  47427  sge0ltfirpmpt2  47435  sge0isummpt2  47441  sge0xaddlem2  47443  sge0xadd  47444  nnfoctbdjlem  47464  meadjuni  47466  meadjiun  47475  voliunsge0lem  47481  meaiuninclem  47489  meaiunincf  47492  meaiuninc3v  47493  meaiuninc3  47494  meaiininclem  47495  meaiininc  47496  omeunile  47514  isomenndlem  47539  ovn0lem  47574  ovnsubaddlem1  47579  hoidmvlelem2  47605  hoidmvlelem3  47606  hoidmvlelem4  47607  hoidmvle  47609  hspmbllem2  47636  hoimbl2  47674  vonhoire  47681  vonicclem2  47693  vonn0ioo2  47699  vonn0icc2  47701  salpreimagelt  47716  salpreimalegt  47718  pimdecfgtioc  47724  pimincfltioc  47725  pimincfltioo  47727  salpreimagtge  47734  salpreimaltle  47735  salpreimagtlt  47739  incsmf  47751  decsmf  47776  smflimlem1  47780  smflimlem2  47781  smflimlem3  47782  smflimlem4  47783  smfpimcclem  47816  funressnmo  48115  fcoresf1  48138  aiota0def  48165  euoreqb  48178  2reu8i  48182  2reuimp0  48183  funressndmafv2rn  48292  funressnbrafv2  48313  funbrafv2  48316  smonoord  48446  elsetpreimafvbi  48472  iccpartgt  48508  iccelpart  48514  iccpartiun  48515  icceuelpartlem  48516  icceuelpart  48517  iccpartnel  48519  fargshiftf1  48522  ichexmpl2  48551  ichnreuop  48553  ichreuopeq  48554  sprsymrelfolem2  48574  prproropf1olem4  48587  paireqne  48592  reupr  48603  reuopreuprim  48607  fmtnofac2  48653  fmtnofac1  48654  prmdvdsfmtnof1lem2  48669  perfectALTVlem2  48819  nfermltl8rev  48839  nfermltl2rev  48840  sbgoldbwt  48874  sbgoldbst  48875  sgoldbeven3prm  48880  sbgoldbm  48881  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  evengpop3  48895  evengpoap3  48896  bgoldbnnsum3prm  48901  bgoldbtbndlem4  48905  bgoldbtbnd  48906  tgblthelfgott  48912  tgoldbach  48914  grimuhgr  48984  grimcnv  48985  isuspgrimlem  48992  isubgr3stgrlem4  49066  isubgr3stgrlem6  49068  isubgr3stgrlem7  49069  gpgedg2ov  49163  gpgedg2iv  49164  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  pgnbgreunbgrlem5lem1  49217  pgnbgreunbgrlem5lem2  49218  pgnbgreunbgrlem5lem3  49219  pgnbgreunbgr  49222  idomnzd  49442  ply1mulgsumlem2  49498  islininds  49557  linindslinci  49559  lindslinindsimp1  49568  linds0  49576  lindsrng01  49579  snlindsntorlem  49581  snlindsntor  49582  ldepsnlinc  49619  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdiglem1  49732  nn0sumshdiglem2  49733  nn0sumshdig  49734  itschlc0yqe  49871  f1mo  49962  iscnrm3lem5  50044  iscnrm3r  50055  isprsd  50062  lubeldm2d  50065  glbeldm2d  50066  joindm2  50075  meetdm2  50077  ipolublem  50093  ipolub  50095  ipoglblem  50096  ipoglb  50098  oppcendc  50125  oppcthinendcALT  50548  functhinclem2  50552  fullthinc  50557  fullthinc2  50558  euendfunc  50633  alsbid  50897  cbvals  50900  nellindf  50969