Theorem imbi12d 344

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imbi12  346  ifpbi123d  1079  nfbiit  1853  nfbidv  1924  sbjust  2067  nfbidf  2232  cbvsbvf  2368  drnf1v  2376  drnf1  2448  mo4  2567  cbvmovw  2603  cbvmow  2604  axextg  2711  rspw  3215  cbvralvw  3216  cbvralfw  3278  raleqbidv  3312  cbvraldva2  3314  sbralie  3316  sbralieOLD  3318  cbvralf  3323  ralcom2  3340  vtoclgaf  3520  vtoclga  3521  vtocl2gafOLD  3524  vtocl3gafOLD  3526  vtocl3gaOLD  3528  vtocl4gaOLD  3531  rspct  3551  rspc  3553  rspc2gv  3575  rexraleqim  3590  ralab2  3644  nelrdva  3652  mob2  3662  mob  3664  morex  3666  reu7  3679  reu8  3680  reu2eqd  3683  cdeqim  3720  sbcimg  3778  sbcim1  3783  sbceqal  3791  csbhypf  3866  cbvralcsf  3880  dfssf  3913  reldisj  4394  ralidmw  4457  reusngf  4619  rexreusng  4624  reuprg0  4647  elpreqpr  4811  unissb  4884  intss1  4906  intmin  4911  dftr2c  5196  trel  5201  zfpow  5304  reusv2lem4  5339  reusv3i  5342  rext  5396  opth  5425  copsexgw  5439  copsexg  5440  poeq1  5536  pocl  5541  swopolem  5543  swopo  5544  isso2i  5570  vtoclr  5688  poinxp  5706  posn  5711  ssrel  5733  ssrel2  5735  ssrelrel  5746  relop  5800  cotrg  6069  cnvsym  6072  reu3op  6251  reuop  6252  dfpo2  6255  preddowncl  6291  frpoinsg  6302  ordelord  6340  iota5  6476  dffun2  6503  sbcfung  6517  funopg  6527  brprcneu  6825  brprcneuALT  6826  tz6.12f  6860  funbrfv  6883  ssimaexg  6921  fvmptf  6964  fvelrn  7023  fprg  7103  dff13f  7204  f1veqaeq  7205  fpropnf1  7216  f1ounsn  7221  nf1const  7253  soisores  7276  soisoi  7277  isofrlem  7289  isopolem  7294  weniso  7303  riota5f  7346  imbrov2fvoveq  7386  oprabidw  7392  oprabid  7393  f1opr  7417  ovmpos  7509  ov2gf  7510  ov3  7524  caovcan  7565  caovordig  7566  caofrss  7664  caoftrn  7666  tfisg  7799  tfis  7800  tfisi  7804  tfindsg  7806  tfindsg2  7807  tfindes  7808  dfom2  7813  limomss  7816  nnlim  7825  peano5  7838  findsg  7842  findes  7845  resf1extb  7879  f1oweALT  7919  dfoprab4f  8003  offval22  8032  f1o2ndf1  8066  frxp  8070  poxp  8072  frpoins3xpg  8084  frpoins3xp3g  8085  poxp2  8087  frxp2  8088  xpord2indlem  8091  poxp3  8094  frxp3  8095  xpord3inddlem  8098  suppfnss  8133  onfununi  8275  smoel  8294  smogt  8301  tfrlem1  8309  tz7.48lem  8374  tz7.49  8378  oawordeu  8484  omordi  8495  oeordi  8517  nnmordi  8561  omabs  8581  nneob  8586  omsmolem  8587  qsel  8737  eroveu  8753  ecopovtrn  8761  ixpsnf1o  8880  fundmeng  8973  sbth  9029  limensuc  9086  findcard  9092  findcard2  9093  findcard2d  9095  pssnn  9097  ssfi  9101  sbthfi  9127  nneneq  9134  php  9135  unxpdom  9163  findcard3  9187  ac6sfi  9188  frfi  9189  domunfican  9226  fiint  9231  iunfi  9247  finsschain  9263  dffi3  9338  marypha1lem  9340  marypha1  9341  supeq3  9356  supeq123d  9357  supmo  9359  suplub  9367  supisolem  9381  eqinf  9392  infval  9394  infmo  9404  ordiso2  9424  ordtypelem7  9433  wemaplem1  9455  wemaplem2  9456  zfregcl  9503  zfregclOLD  9504  elirrv  9506  inf0  9536  inf3lem1  9543  zfinf  9554  axinf2  9555  dfom3  9562  elom3  9563  cantnfval2  9584  cantnfle  9586  cantnflt  9587  cantnfp1lem3  9595  oemapvali  9599  cantnflem1c  9602  cantnflem1  9604  cantnf  9608  wemapwe  9612  cnfcom  9615  ttrclss  9635  ttrclselem2  9641  setind  9662  setinds  9664  frmin  9667  frinsg  9669  r1sdom  9692  r1ordg  9696  rankonidlem  9746  rankunb  9768  bnd2  9811  infxpenlem  9929  infxpenc2  9938  dfac8alem  9945  dfac8clem  9948  indcardi  9957  alephordi  9990  alephinit  10011  alephfp  10024  aceq3lem  10036  dfac5lem4  10042  dfac5lem4OLD  10044  dfac5  10045  dfac2b  10047  dfac9  10053  dfac12lem2  10061  dfac12lem3  10062  kmlem1  10067  kmlem4  10070  kmlem10  10076  kmlem12  10078  kmlem13  10079  pwsdompw  10119  ackbij1lem16  10150  cfslb2n  10184  cfsmolem  10186  sornom  10193  fin2i  10211  infpssrlem4  10222  isfin2-2  10235  isfin3ds  10245  fin23lem17  10254  fin23lem32  10260  fin23lem34  10262  fin23lem35  10263  fin23lem39  10266  fin23lem41  10268  isf32lem2  10270  isf33lem  10282  isf34lem4  10293  isf34lem6  10296  fin1a2lem10  10325  axcc2lem  10352  axcc3  10354  axcc4dom  10357  dominf  10361  axdc2lem  10364  axdc3lem2  10367  ac6sg  10404  zorn2lem7  10418  zornn0g  10421  ttukeylem5  10429  ttukeylem6  10430  axdclem  10435  dominfac  10490  axrepndlem1  10509  axrepndlem2  10510  axunndlem1  10512  axunnd  10513  axpowndlem2  10515  axpowndlem3  10516  axpowndlem4  10517  axregndlem2  10520  axregnd  10521  axinfndlem1  10522  axinfnd  10523  axacndlem4  10527  axacndlem5  10528  axacnd  10529  zfcndpow  10533  zfcndinf  10535  fpwwe2lem4  10551  fpwwe2lem7  10554  fpwwe2lem11  10558  pwfseqlem4a  10578  pwfseqlem4  10579  pwfseqlem5  10580  pwfseq  10581  wunfi  10638  wunex2  10655  inar1  10692  rankcf  10694  tskord  10697  grudomon  10734  grur1a  10736  axgroth6  10745  axgroth3  10748  axgroth4  10749  eltskm  10760  indpi  10824  pinq  10844  nqereu  10846  prcdnq  10910  prnmax  10912  ltsopr  10949  prlem936  10964  ltsosr  11011  recexsrlem  11020  mulgt0sr  11022  map2psrpr  11027  supsrlem  11028  axrrecex  11080  axpre-lttrn  11083  axpre-mulgt0  11085  axpre-sup  11086  axsup  11215  dedekind  11303  ltordlem  11669  ltord1  11670  wloglei  11676  squeeze0  12053  infm3  12109  nnsub  12215  nnunb  12427  peano5uzti  12613  fzind  12621  uzind4s  12852  uzind4s2  12853  zmax  12889  zbtwnre  12890  xmulasslem  13231  xrsupsslem  13253  xrinfmsslem  13254  xrub  13258  infmremnf  13290  injresinj  13740  om2uzlti  13906  uzindi  13938  axdc4uz  13940  ssnn0fi  13941  rabssnn0fi  13942  suppssfz  13950  seqp1  13972  seqcl2  13976  seqfveq2  13980  seqshft2  13984  monoord  13988  seqsplit  13991  seqf1olem2  13998  seqf1o  13999  seqid2  14004  seqhomo  14005  seqof2  14016  expcl2lem  14029  facdiv  14243  facwordi  14245  faclbnd4lem2  14250  hashnn0n0nn  14347  hashf1lem2  14412  seqcoll  14420  fi1uzind  14463  brfi1indALT  14466  wrdind  14678  wrd2ind  14679  swrdccatin1  14681  swrdccat3blem  14695  reuccatpfxs1lem  14702  repswccat  14742  cshf1  14766  trclfvcotr  14965  relexprelg  14994  rtrclreclem4  15017  relexpindlem  15019  ello1mpt  15477  o1co  15542  o1compt  15543  rlimcn3  15546  climcn2  15549  subcn2  15551  o1of2  15569  fsumclf  15694  fsumsplitf  15698  fsumsplit1  15701  fsum2d  15727  modfsummod  15751  fsumabs  15758  telfsumo  15759  fsumrlim  15768  fsumo1  15769  o1fsum  15770  fsumiun  15778  prodfdiv  15855  fprod2d  15940  fproddivf  15946  fprodsplitf  15947  fprodsplit1f  15949  rpnnen2lem10  16184  sqrt2irr  16210  dvdsle  16273  divalglem7  16362  divalglem8  16363  ndvdssub  16372  gcdcllem1  16462  dfgcd2  16509  algcvg  16539  algcvga  16542  algfx  16543  lcmgcdlem  16569  lcmdvds  16571  lcmf  16596  lcmfunsnlem1  16600  lcmfunsnlem2lem1  16601  lcmfunsnlem  16604  lcmfdvds  16605  lcmfun  16608  coprmgcdb  16612  coprmdvds1  16615  coprmdvds2  16617  coprmprod  16624  coprmproddvds  16626  prmind2  16648  dvdsprime  16650  nprm  16651  dvdsprm  16667  exprmfct  16668  coprm  16675  isprm6  16678  prmfac1  16684  eulerthlem2  16746  pcqmul  16818  pcqcl  16821  pc2dvds  16844  pcz  16846  prmpwdvds  16869  infpn2  16878  vdwlem12  16957  ramub2  16979  rami  16980  ramcl  16994  prmdvdsprmop  17008  prmlem0  17070  mreintcl  17551  ismred2  17559  mrissmrcd  17600  mreexexlemd  17604  iscatd2  17641  moni  17697  yoniso  18245  isprs  18256  prslem  18257  drsdirfi  18265  ispos  18274  posi  18277  isposd  18282  pospropd  18285  lubfval  18308  lublecllem  18318  glbfval  18321  joinle  18344  meetle  18358  poslubmo  18369  posglbmo  18370  resspos  18389  lubl  18472  lubun  18475  clatleglb  18478  ipodrsima  18501  acsdrsel  18503  isacs4lem  18504  isacs5lem  18505  acsdrscl  18506  mreclatBAD  18523  pslem  18532  dirtr  18562  chnind  18581  mndind  18790  mhmlem  19032  isnsg2  19125  ghmf1  19215  orbsta  19282  symgextf1  19390  gsmsymgrfix  19397  gsmsymgreq  19401  symggen  19439  psgnunilem4  19466  sylow1lem1  19567  sylow2alem2  19587  sylow2a  19588  lsmmod  19644  lsmdisj2  19651  efgsrel  19703  efgredlemd  19713  efgredlem  19716  efgred  19717  gsumzaddlem  19890  gsummptnn0fz  19955  gsummptnn0fzfv  19956  telgsumfzs  19958  telgsums  19962  dprdval  19974  dprddisj2  20010  ablfac1eulem  20043  pgpfac1lem1  20045  pgpfac1lem5  20050  pgpfac1  20051  pgpfaclem2  20053  pgpfac  20055  isomnd  20092  omndadd  20097  gsumle  20114  irredmul  20403  islring  20511  lringuplu  20515  rrgval  20668  rrgeq0i  20670  isdomn  20676  domneq0  20679  isdomn4  20687  domnlcanb  20691  domnrcanb  20693  isdrngrd  20737  isdrngrdOLD  20739  sdrgacs  20772  isorng  20832  orngmul  20836  islbs3  21148  rngqiprngimf1lem  21287  cnsubrglem  21409  prmirredlem  21465  znfld  21553  znrrg  21558  cygznlem3  21562  isphl  21621  ipeq0  21631  isphld  21647  phlpropd  21648  lsmcss  21685  frlmphl  21774  frlmup1  21791  lindfrn  21814  islindf4  21831  islindf5  21832  mplsubglem  21990  mpllsslem  21991  mplcoe1  22028  mplcoe5  22031  mpfind  22106  ismhp3  22121  coe1fzgsumd  22282  gsummoncoe1  22286  pf1ind  22333  evl1gsumd  22335  dmatelnd  22474  mat1scmat  22517  mdetdiaglem  22576  mdetralt  22586  mdetralt2  22587  mdetunilem1  22590  mdetunilem2  22591  mdetunilem3  22592  mdetunilem4  22593  mdetunilem9  22598  smadiadetr  22653  pmatcoe1fsupp  22679  mp2pm2mplem4  22787  uniopn  22875  fiinopn  22879  epttop  22987  clsndisj  23053  elcls3  23061  neiptoptop  23109  neiptopnei  23110  cnpval  23214  iscnp  23215  cnpimaex  23234  lmcvg  23240  cnprest  23267  cnprest2  23268  lmss  23276  lmff  23279  t0sep  23302  hausnei  23306  isnrm2  23336  t1sep2  23347  isreg2  23355  iscmp  23366  cmpcov  23367  cmpsublem  23377  cmpsub  23378  tgcmp  23379  uncmp  23381  fiuncmp  23382  hauscmplem  23384  cmpfi  23386  cmpfii  23387  dfconn2  23397  connsuba  23398  connsub  23399  nconnsubb  23401  1stcclb  23422  1stcfb  23423  2ndc1stc  23429  1stcrest  23431  1stcelcls  23439  restnlly  23460  lly1stc  23474  comppfsc  23510  kgenval  23513  kgeni  23515  kgencn2  23535  ptcldmpt  23592  ptclsg  23593  dfac14lem  23595  dfac14  23596  txcnp  23598  ptcnp  23600  hausdiag  23623  txlm  23626  tx1stc  23628  xkococn  23638  cnmpt12  23645  cnmpt22  23652  kqt0lem  23714  isr0  23715  regr1lem2  23718  kqreglem1  23719  r0sep  23726  ptcmpfi  23791  elmptrab  23805  isfil  23825  filss  23831  isufil2  23886  cfinufil  23906  rnelfm  23931  fmfnfmlem2  23933  fmfnfmlem4  23935  flimopn  23953  flimrest  23961  flftg  23974  cnpflf  23979  txflf  23984  fclsopni  23993  fclsrest  24002  fclscf  24003  flimfnfcls  24006  fcfnei  24013  alexsublem  24022  alexsubb  24024  alexsubALTlem3  24027  alexsubALTlem4  24028  alexsubALT  24029  cnextcn  24045  cnextfres1  24046  tgpt0  24097  qustgplem  24099  tsmsi  24112  tsmssubm  24121  tsmsres  24122  tsmsf1o  24123  tsmsxp  24133  ustssel  24184  ust0  24198  ustuqtop4  24222  ucnima  24258  ucncn  24262  iscusp  24276  cuspcvg  24278  imasdsf1olem  24351  blssps  24402  blss  24403  metss  24486  comet  24491  metcnp3  24518  metcnp2  24520  txmetcnp  24525  metuel2  24543  metucn  24549  nrmmetd  24552  nlmvscn  24665  nrginvrcn  24670  nmolb  24695  xrge0tsms  24813  mpomulcn  24847  divcn  24848  fsumcn  24850  elcncf2  24870  cncfi  24874  mulc1cncf  24885  cncfmet  24889  xrhmeo  24926  bndth  24938  nmoleub2lem2  25096  nmoleub3  25099  ipcn  25226  lmmbr  25238  caucfil  25263  pmltpc  25430  ovolfiniun  25481  ovolicc2lem3  25499  ovolicc2  25502  mblsplit  25512  finiunmbl  25524  volfiniun  25527  voliunlem3  25532  ioorinv  25556  ioorcl  25557  dyadmax  25578  dyadmbllem  25579  dyadmbl  25580  opnmbllem  25581  volcn  25586  vitalilem2  25589  vitalilem3  25590  vitali  25593  i1fd  25661  itg2seq  25722  itg2addlem  25738  itgfsum  25807  ellimc3  25859  dvbsss  25882  dvnres  25911  dvmptfsum  25955  dvferm1lem  25964  dvferm2lem  25966  rolle  25970  c1lip1  25977  lhop1lem  25993  lhop1  25994  dvfsumlem2  26007  dvfsumlem4  26009  dvfsumrlim  26011  dvfsum2  26014  ftc1a  26017  ftc1lem6  26021  mdegleb  26042  mdeglt  26043  deg1leb  26073  deg1lt  26075  ply1divex  26115  fta1glem2  26147  fta1g  26148  plyco0  26170  plyeq0lem  26188  coeeq2  26220  dgrle  26221  dgrcolem2  26252  dgrco  26253  plydivlem4  26276  plydivex  26277  fta1lem  26287  fta1  26288  vieta1lem2  26291  vieta1  26292  aalioulem2  26313  aalioulem4  26315  abelth  26422  cxpcn3  26728  rlimcnp  26945  xrlimcnp  26948  cxploglim  26958  scvxcvx  26966  jensen  26969  lgamgulmlem2  27010  wilthlem2  27049  wilthlem3  27050  fta  27060  mpodvdsmulf1o  27174  dvdsmulf1o  27176  perfectlem2  27210  dchrelbas3  27218  dchrelbas4  27223  dchrn0  27230  bcmono  27257  lgsdir2lem4  27308  lgsdchr  27335  gausslemma2dlem0i  27344  lgseisenlem2  27356  lgsquad2lem2  27365  2sqlem6  27403  2sqlem8  27406  2sqlem10  27408  dchrisumlema  27468  dchrisumlem2  27470  dchrisumlem3  27471  nosupprefixmo  27681  noinfprefixmo  27682  nosupcbv  27683  nosupdm  27685  nosupfv  27687  nosupres  27688  nosupbnd1lem1  27689  nosupbnd1lem3  27691  nosupbnd1lem5  27693  nosupbnd2  27697  noinfcbv  27698  noinfdm  27700  noinffv  27702  noinfres  27703  noinfbnd1lem1  27704  noinfbnd1lem3  27706  noinfbnd1lem5  27708  noinfbnd2  27712  nocvxminlem  27763  madebdaylemold  27907  madebdaylemlrcut  27908  madebday  27909  lrrecpo  27950  addsproplem1  27978  addsprop  27985  leadds1  27998  negsproplem1  28037  negsprop  28044  mulsproplemcbv  28124  mulsproplem1  28125  mulsprop  28139  precsexlem8  28223  precsexlem9  28224  precsexlem11  28226  precsex  28227  bdayons  28285  addonbday  28288  onsfi  28365  n0subs  28372  oldfib  28386  eln0zs  28409  bdaypw2n0bndlem  28472  bdaypw2n0bnd  28473  bdayfinbndcbv  28475  bdayfinbndlem1  28476  bdayfinbndlem2  28477  bdayfinbnd  28478  istrkgb  28540  istrkgcb  28541  istrkge  28542  axtgcgrid  28548  axtg5seg  28550  axtgbtwnid  28551  axtgpasch  28552  axtgcont1  28553  axtgeucl  28557  iscgrglt  28599  tgcgr4  28616  axcgrtr  29001  gropd  29117  grstructd  29118  upgredg2vtx  29227  upgredgpr  29228  edglnl  29229  numedglnl  29230  usgredg2vtxeuALT  29308  nbgr2vtx1edg  29436  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  32647  iinabrex  32657  ssrelf  32706  fmptcof2  32748  acunirnmpt  32750  acunirnmpt2  32751  acunirnmpt2f  32752  aciunf1lem  32753  suppovss  32772  fz1nntr  32893  nn0min  32912  fsumiunle  32920  wrdt2ind  33031  ressprs  33044  toslublem  33050  tosglblem  33052  mntoval  33060  ismntd  33062  dfmgc2lem  33073  dfmgc2  33074  xrge0tsmsd  33152  fzto1st  33182  psgnfzto1st  33184  submarchi  33265  archirng  33267  archiexdiv  33269  archiabllem1a  33270  archiabllem2a  33273  archiabl  33277  isarchiofld  33278  gsumvsca1  33305  gsumvsca2  33306  elrgspnlem4  33324  domnpropd  33356  domnlcanOLD  33359  linds2eq  33459  isprmidl  33516  prmidl  33518  prmidlc  33526  ssdifidlprm  33536  ismxidl  33540  mxidlmax  33543  rprmval  33594  isrprm  33595  rprmdvds  33597  rprmdvdsprod  33612  1arithidomlem1  33613  1arithidom  33615  1arithufdlem3  33624  dfufd2lem  33627  lbsdiflsp0  33789  fedgmullem1  33792  fedgmullem2  33793  fldext2chn  33891  constrmon  33907  submateq  33972  lmatfval  33977  lmatcl  33979  iscref  34007  crefi  34010  pcmplfin  34023  xrge0iifiso  34098  esumcvg  34249  esum2dlem  34255  sigaclcu  34280  sigaclci  34295  unelsiga  34297  unelldsys  34321  sigapildsys  34325  ldgenpisyslem1  34326  fiunelros  34337  measvun  34372  measiun  34381  carsgmon  34477  carsgsigalem  34478  carsgclctunlem2  34482  carsgclctun  34484  pmeasmono  34487  pmeasadd  34488  sibfof  34503  sitgclg  34505  eulerpartlemgvv  34539  signsply0  34714  signstfvneq0  34735  breprexp  34796  hgt749d  34812  istrkg2d  34829  axtgupdim2ALTV  34831  bnj1385  34993  bnj110  35019  bnj222  35044  bnj229  35045  bnj590  35071  bnj865  35084  bnj849  35086  bnj981  35111  bnj1014  35122  bnj1015  35123  bnj1112  35144  bnj1118  35145  bnj1123  35147  bnj1128  35151  bnj1125  35153  bnj1148  35157  bnj1154  35160  bnj1326  35187  bnj1384  35193  bnj1489  35217  bnj1497  35221  funen1cnv  35250  r1filimi  35265  trssfir1om  35274  r1omhfb  35275  setindregs  35293  trssfir1omregs  35299  r1omhfbregs  35300  onvf1odlem2  35305  f1resfz0f1d  35315  cplgredgex  35322  acycgrcycl  35348  subfacp1lem6  35386  erdszelem9  35400  kur14lem9  35415  sconnpht  35430  cvmsss2  35475  cvmliftlem7  35492  cvmliftlem10  35495  fmlasuc  35587  gonar  35596  goalr  35598  mclsrcl  35762  mclsssvlem  35763  mclsval  35764  mclsax  35770  mclsind  35771  mclsppslem  35784  iota5f  35925  fununiq  35970  dfon2lem3  35984  dfon2lem4  35985  dfon2lem5  35986  dfon2lem6  35987  dfon2lem7  35988  dfon2lem8  35989  dfon2  35991  btwnconn1lem11  36298  linethru  36354  fwddifnp1  36366  rankelg  36369  rankeq1o  36372  sbequbidv  36415  cbvralvw2  36427  cbvmodavw  36451  cbvsbdavw  36455  cbvsbdavw2  36456  subtr  36515  subtr2  36516  trer  36517  nn0prpwlem  36523  nn0prpw  36524  neibastop2lem  36561  filnetlem4  36582  axtco1from2  36676  axtcond  36679  axuntco  36680  dfttc4lem2  36730  dfttc4  36731  mh-setindnd  36738  regsfromregtco  36739  regsfromsetind  36740  mh-inf3f1  36742  mh-unprimbi  36745  mh-infprim2bi  36748  bj-hbxfrbi  36926  bj-hbyfrbi  36927  bj-ssblem1  36967  bj-ssblem2  36968  bj-ax12  36970  irrdiff  37659  relowlssretop  37696  rdgeqoa  37703  rdgssun  37711  exrecfnlem  37712  finxpreclem6  37729  pibp19  37747  pibt2  37750  wl-ax12v2cl  37839  wl-mo3t  37918  wl-sb8mot  37922  wl-sb8motv  37923  finixpnum  37943  matunitlindflem1  37954  ptrest  37957  poimirlem13  37971  poimirlem14  37972  poimirlem17  37975  poimirlem18  37976  poimirlem20  37978  poimirlem21  37979  poimirlem22  37980  poimirlem24  37982  poimirlem25  37983  poimirlem26  37984  poimirlem28  37986  poimirlem30  37988  poimirlem31  37989  poimirlem32  37990  poimir  37991  heicant  37993  mblfinlem1  37995  mblfinlem2  37996  mblfinlem3  37997  voliunnfl  38002  volsupnfl  38003  mbfresfi  38004  itg2addnclem3  38011  ftc1cnnc  38030  ftc1anclem7  38037  ftc1anc  38039  sdclem2  38080  fdc  38083  fdc1  38084  neificl  38091  mettrifi  38095  sstotbnd2  38112  cntotbnd  38134  heibor1lem  38147  bfp  38162  isass  38184  ismgmOLD  38188  isexid2  38193  iscringd  38336  ispridl  38372  pridl  38375  ismaxidl  38378  maxidlmax  38381  ispridlc  38408  pridlc  38409  dmnnzd  38413  relcnveq2  38667  ecin0  38690  elrelscnveq2  38967  elsymrels3  38976  eltrrels3  39002  eleqvrels3  39015  eqvrelqsel  39038  disjimeceqim2  39143  eldisjim3  39153  eldisjlem19  39251  eldisjsim3  39275  axc11n-16  39401  ax12eq  39404  ax12el  39405  ax12inda  39411  ax12v2-o  39412  fsumshftd  39415  riotasv2d  39420  lshpdisj  39450  lsmsatcv  39473  lsat0cv  39496  lcvexchlem4  39500  lcvexchlem5  39501  l1cvpat  39517  isopos  39643  oposlem  39645  isoml  39701  omllaw  39706  isatl  39762  atlex  39779  iscvlat  39786  cvlexch1  39791  glbconN  39840  hlsuprexch  39844  ps-1  39940  3atlem5  39950  psubspi  40210  llnexchb2  40332  elpcliN  40356  pclfinclN  40413  ldilval  40576  ltrnfset  40580  ltrnset  40581  ltrnu  40584  trlfset  40623  trlset  40624  trlval2  40626  cdleme25cv  40821  cdleme31so  40842  cdleme31fv  40853  cdlemefrs29bpre0  40859  cdleme32fva  40900  cdleme40v  40932  trlord  41032  cdlemkid3N  41396  cdlemkid4  41397  dihffval  41693  dihfval  41694  dihval  41695  lpolconN  41950  mapdordlem2  42100  hdmapfval  42290  hdmapval  42291  hdmapval2  42295  aks4d1p7  42539  isprimroot  42549  primrootlekpowne0  42561  sticksstones1  42602  sticksstones2  42603  sticksstones10  42611  sticksstones12a  42613  aks6d1c6lem3  42628  indstrd  42649  unitscyglem2  42652  unitscyglem3  42653  unitscyglem4  42654  nnn1suc  42721  fsuppind  43040  eu6w  43126  ismrcd1  43147  ismrcd2  43148  ismrc  43150  isnacs3  43159  nacsfix  43161  mzpcompact2  43201  fphpd  43265  fphpdo  43266  monotuz  43390  monotoddzzfi  43391  monotoddzz  43392  oddcomabszz  43393  zindbi  43395  setindtrs  43474  dford3lem2  43476  ttac  43485  dnnumch1  43493  fnwe2lem2  43500  aomclem3  43505  aomclem6  43508  aomclem8  43510  dfac11  43511  dfac21  43515  islssfg2  43520  hbtlem5  43577  hbt  43579  flcidc  43619  mendlmod  43638  unielss  43667  rababg  44022  elmapintrab  44024  iunrelexpuztr  44167  frege92  44403  frege104  44415  ntrkbimka  44486  ntrk0kbimka  44487  neik0pk1imk0  44495  isotone1  44496  isotone2  44497  ntrclsiso  44515  ntrclskb  44517  ntrneiiso  44539  ntrneik3  44544  ntrneix3  44545  gneispacess2  44594  grur1cld  44680  scottabf  44688  ismnu  44709  mnuop23d  44714  mnuunid  44725  ismnushort  44749  dvgrat  44760  cvgdvgrat  44761  binomcxplemnotnn0  44804  pm14.122b  44871  sbiota1  44882  relprel  45399  relpfrlem  45401  modelaxreplem1  45426  modelaxreplem2  45427  modelaxrep  45429  omssaxinf2  45436  modelac8prim  45440  permaxinf2lem  45460  permac8prim  45462  nregmodel  45465  fnchoice  45481  fiiuncl  45517  iunincfi  45545  disjf1  45634  wessf1ornlem  45636  disjinfi  45643  axccdom  45672  dmrelrnrel  45676  axccd  45679  monoords  45751  fperiodmullem  45757  supxrgere  45784  supxrgelem  45788  supxrge  45789  xrlexaddrp  45803  infxr  45817  infleinf  45822  supxrleubrnmptf  45900  monoordxrv  45930  monoordxr  45931  monoord2xr  45933  fsummulc1f  46022  fsumnncl  46023  fsumf1of  46025  fsumreclf  46027  fsumlessf  46028  fsumsermpt  46030  fmul01  46031  fmulcl  46032  fmuldfeqlem1  46033  fmuldfeq  46034  fmul01lt1lem1  46035  fmul01lt1lem2  46036  fprodexp  46045  fprodabs2  46046  fprodcnlem  46050  climmulf  46055  climexp  46056  climsuse  46059  climrecf  46060  climinff  46062  climaddf  46066  mullimc  46067  mullimcf  46074  limcperiod  46079  sumnnodd  46081  lptre2pt  46089  limsupre  46090  neglimc  46096  addlimc  46097  0ellimcdiv  46098  limclner  46100  climsubmpt  46109  climreclf  46113  climeldmeqmpt  46117  climfveqmpt  46120  fnlimfvre  46123  climfveqf  46129  climfveqmpt3  46131  climeldmeqf  46132  limsupref  46134  limsupbnd1f  46135  climeqf  46137  climeldmeqmpt3  46138  climinf2  46156  limsupubuz  46162  climinf2mpt  46163  climinfmpt  46164  limsupmnf  46170  limsupequz  46172  limsupre2  46174  limsupequzmptf  46180  limsupre3  46182  lmbr3  46196  cnrefiisp  46279  xlimxrre  46280  xlimmnfvlem1  46281  xlimpnfvlem1  46285  climxlim2lem  46294  cncfshift  46323  cncfperiod  46328  icccncfext  46336  fprodcncf  46349  fperdvper  46368  dvmptmulf  46386  dvnmptdivc  46387  dvnmul  46392  dvmptfprod  46394  dvnprodlem1  46395  dvnprodlem2  46396  dvnprodlem3  46397  iblspltprt  46422  itgspltprt  46428  stoweidlem3  46452  stoweidlem4  46453  stoweidlem6  46455  stoweidlem8  46457  stoweidlem15  46464  stoweidlem16  46465  stoweidlem17  46466  stoweidlem19  46468  stoweidlem20  46469  stoweidlem22  46471  stoweidlem23  46472  stoweidlem26  46475  stoweidlem27  46476  stoweidlem30  46479  stoweidlem31  46480  stoweidlem32  46481  stoweidlem34  46483  stoweidlem35  46484  stoweidlem42  46491  stoweidlem43  46492  stoweidlem48  46497  stoweidlem50  46499  stoweidlem51  46500  stoweidlem57  46506  stoweidlem59  46508  stoweidlem62  46511  wallispilem3  46516  dirkercncflem2  46553  fourierdlem11  46567  fourierdlem12  46568  fourierdlem15  46571  fourierdlem16  46572  fourierdlem21  46577  fourierdlem34  46590  fourierdlem41  46597  fourierdlem42  46598  fourierdlem46  46601  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem51  46606  fourierdlem68  46623  fourierdlem71  46626  fourierdlem72  46627  fourierdlem73  46628  fourierdlem76  46631  fourierdlem79  46634  fourierdlem81  46636  fourierdlem83  46638  fourierdlem86  46641  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem92  46647  fourierdlem94  46649  fourierdlem97  46652  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  fourierdlem112  46667  fourierdlem113  46668  etransclem2  46685  etransclem46  46729  salunicl  46765  saluncl  46766  intsaluni  46778  dfsalgen2  46790  sge0f1o  46831  sge0lempt  46859  sge0iunmptlemfi  46862  sge0p1  46863  sge0fodjrnlem  46865  sge0iunmpt  46867  sge0ltfirpmpt2  46875  sge0isummpt2  46881  sge0xaddlem2  46883  sge0xadd  46884  nnfoctbdjlem  46904  meadjuni  46906  meadjiun  46915  voliunsge0lem  46921  meaiuninclem  46929  meaiunincf  46932  meaiuninc3v  46933  meaiuninc3  46934  meaiininclem  46935  meaiininc  46936  omeunile  46954  isomenndlem  46979  ovn0lem  47014  ovnsubaddlem1  47019  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  hoidmvle  47049  hspmbllem2  47076  hoimbl2  47114  vonhoire  47121  vonicclem2  47133  vonn0ioo2  47139  vonn0icc2  47141  salpreimagelt  47156  salpreimalegt  47158  pimdecfgtioc  47164  pimincfltioc  47165  pimincfltioo  47167  salpreimagtge  47174  salpreimaltle  47175  salpreimagtlt  47179  incsmf  47191  decsmf  47216  smflimlem1  47220  smflimlem2  47221  smflimlem3  47222  smflimlem4  47223  smfpimcclem  47256  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