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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imbi12  346  ifpbi123d  1076  nfbiit  1854  nfbidv  1926  sbjust  2067  nfbidf  2220  sbievg  2361  drnf1v  2370  drnf1vOLD  2371  drnf1  2443  mo4  2566  cbvmovw  2602  cbvmow  2603  axextg  2711  nfcriOLD  2896  rspw  3128  ralcom2  3288  raleqbidv  3327  cbvralfw  3358  cbvralfwOLD  3359  cbvralf  3361  cbvralvw  3372  cbvraldva2  3381  vtoclgaf  3502  vtoclga  3503  vtocl2gaf  3505  vtocl3gaf  3506  vtocl3ga  3507  vtocl4ga  3510  rspct  3537  rspc  3539  rspc2gv  3561  rexraleqim  3569  ralab2  3627  ralab2OLD  3628  nelrdva  3635  mob2  3645  mob  3647  morex  3649  reu7  3662  reu8  3663  reu2eqd  3666  cdeqim  3703  sbcimg  3762  sbcim1  3767  sbceqal  3778  csbhypf  3857  cbvralcsf  3873  dfss2f  3907  reldisj  4382  ralidmw  4435  reusngf  4605  rexreusng  4612  reuprg0  4635  elpreqpr  4794  elintab  4887  intss1  4891  intmin  4896  dfiin2g  4958  trel  5194  zfpow  5284  reusv2lem4  5319  reusv3i  5322  rext  5358  opth  5385  copsexgw  5398  copsexg  5399  poeq1  5497  pocl  5501  poclOLD  5502  swopolem  5504  swopo  5505  isso2i  5529  friOLD  5541  vtoclr  5641  poinxp  5658  posn  5663  ssrel  5683  ssrel2  5685  ssrelrel  5695  relop  5748  reu3op  6184  reuop  6185  dfpo2  6188  predbrg  6213  preddowncl  6224  frpoinsg  6231  wfisgOLD  6242  ordelord  6273  iota5  6401  sbcfung  6442  funopg  6452  brprcneu  6747  fvprc  6748  tz6.12f  6780  funbrfv  6802  ssimaexg  6836  fvmptf  6878  fvelrn  6936  fprg  7009  dff13f  7110  f1veqaeq  7111  fpropnf1  7121  nf1const  7156  soisores  7178  soisoi  7179  isofrlem  7191  isopolem  7196  weniso  7205  riota5f  7241  imbrov2fvoveq  7280  oprabidw  7286  oprabid  7287  f1opr  7309  ovmpos  7399  ov2gf  7400  ov3  7413  caovcan  7454  caovordig  7455  caofrss  7547  caoftrn  7549  tfis  7676  tfisi  7680  tfindsg  7682  tfindsg2  7683  tfindes  7684  dfom2  7689  limomss  7692  nnlim  7701  peano5  7714  findsg  7720  findes  7723  f1oweALT  7788  dfoprab4f  7869  offval22  7899  f1o2ndf1  7934  frxp  7938  poxp  7940  suppfnss  7976  wfrdmclOLD  8119  onfununi  8143  smoel  8162  smogt  8169  tfrlem1  8178  tz7.48lem  8242  tz7.49  8246  oawordeu  8348  omordi  8359  oeordi  8380  nnmordi  8424  omabs  8441  nneob  8446  omsmolem  8447  qsel  8543  eroveu  8559  ecopovtrn  8567  ixpsnf1o  8684  fundmeng  8776  sbth  8833  limensuc  8890  nneneq  8896  php  8897  php2  8898  findcard  8908  findcard2  8909  findcard2d  8911  pssnn  8913  ssfi  8918  sbthfi  8942  unxpdom  8959  pssnnOLD  8969  findcard2OLD  8986  findcard3  8987  ac6sfi  8988  frfi  8989  domunfican  9017  fiint  9021  iunfi  9037  finsschain  9056  dffi3  9120  marypha1lem  9122  marypha1  9123  supeq3  9138  supeq123d  9139  supmo  9141  suplub  9149  supisolem  9162  eqinf  9173  infval  9175  infmo  9184  ordiso2  9204  ordtypelem7  9213  wemaplem1  9235  wemaplem2  9236  zfregcl  9283  inf0  9309  inf3lem1  9316  zfinf  9327  axinf2  9328  dfom3  9335  elom3  9336  cantnfval2  9357  cantnfle  9359  cantnflt  9360  cantnfp1lem3  9368  oemapvali  9372  cantnflem1c  9375  cantnflem1  9377  cantnf  9381  wemapwe  9385  cnfcom  9388  setind  9423  frmin  9438  frinsg  9440  r1sdom  9463  r1ordg  9467  rankonidlem  9517  rankunb  9539  bnd2  9582  infxpenlem  9700  infxpenc2  9709  dfac8alem  9716  dfac8clem  9719  indcardi  9728  alephordi  9761  alephinit  9782  alephfp  9795  aceq3lem  9807  dfac5lem4  9813  dfac5  9815  dfac2b  9817  dfac9  9823  dfac12lem2  9831  dfac12lem3  9832  kmlem1  9837  kmlem4  9840  kmlem10  9846  kmlem12  9848  kmlem13  9849  pwsdompw  9891  ackbij1lem16  9922  cfslb2n  9955  cfsmolem  9957  sornom  9964  fin2i  9982  infpssrlem4  9993  isfin2-2  10006  isfin3ds  10016  fin23lem17  10025  fin23lem32  10031  fin23lem34  10033  fin23lem35  10034  fin23lem39  10037  fin23lem41  10039  isf32lem2  10041  isf33lem  10053  isf34lem4  10064  isf34lem6  10067  fin1a2lem10  10096  axcc2lem  10123  axcc3  10125  axcc4dom  10128  dominf  10132  axdc2lem  10135  axdc3lem2  10138  ac6sg  10175  zorn2lem7  10189  zornn0g  10192  ttukeylem5  10200  ttukeylem6  10201  axdclem  10206  dominfac  10260  axrepndlem1  10279  axrepndlem2  10280  axunndlem1  10282  axunnd  10283  axpowndlem2  10285  axpowndlem3  10286  axpowndlem4  10287  axregndlem2  10290  axregnd  10291  axinfndlem1  10292  axinfnd  10293  axacndlem4  10297  axacndlem5  10298  axacnd  10299  zfcndpow  10303  zfcndinf  10305  fpwwe2lem4  10321  fpwwe2lem7  10324  fpwwe2lem11  10328  pwfseqlem4a  10348  pwfseqlem4  10349  pwfseqlem5  10350  pwfseq  10351  wunfi  10408  wunex2  10425  inar1  10462  rankcf  10464  tskord  10467  grudomon  10504  grur1a  10506  axgroth6  10515  axgroth3  10518  axgroth4  10519  eltskm  10530  indpi  10594  pinq  10614  nqereu  10616  prcdnq  10680  prnmax  10682  ltsopr  10719  prlem936  10734  ltsosr  10781  recexsrlem  10790  mulgt0sr  10792  map2psrpr  10797  supsrlem  10798  axrrecex  10850  axpre-lttrn  10853  axpre-mulgt0  10855  axpre-sup  10856  axsup  10981  dedekind  11068  ltordlem  11430  ltord1  11431  wloglei  11437  squeeze0  11808  infm3  11864  nnsub  11947  nnunb  12159  peano5uzti  12340  fzind  12348  eluzadd  12542  eluzsub  12543  uzind4s  12577  uzind4s2  12578  zmax  12614  zbtwnre  12615  xmulasslem  12948  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  infmremnf  13006  injresinj  13436  om2uzlti  13598  uzindi  13630  axdc4uz  13632  ssnn0fi  13633  rabssnn0fi  13634  suppssfz  13642  seqp1  13664  seqcl2  13669  seqfveq2  13673  seqshft2  13677  monoord  13681  seqsplit  13684  seqf1olem2  13691  seqf1o  13692  seqid2  13697  seqhomo  13698  seqof2  13709  expcl2lem  13722  facdiv  13929  facwordi  13931  faclbnd4lem2  13936  hashnn0n0nn  14034  hashf1lem2  14098  seqcoll  14106  fi1uzind  14139  brfi1indALT  14142  wrdind  14363  wrd2ind  14364  swrdccatin1  14366  swrdccat3blem  14380  reuccatpfxs1lem  14387  repswccat  14427  cshf1  14451  trclfvcotr  14648  relexprelg  14677  rtrclreclem4  14700  relexpindlem  14702  ello1mpt  15158  o1co  15223  o1compt  15224  rlimcn3  15227  climcn2  15230  subcn2  15232  o1of2  15250  fsumclf  15378  fsumsplitf  15382  fsumsplit1  15385  fsum2d  15411  modfsummod  15434  fsumabs  15441  telfsumo  15442  fsumrlim  15451  fsumo1  15452  o1fsum  15453  fsumiun  15461  prodfdiv  15536  fprod2d  15619  fproddivf  15625  fprodsplitf  15626  fprodsplit1f  15628  rpnnen2lem10  15860  sqrt2irr  15886  dvdsle  15947  divalglem7  16036  divalglem8  16037  ndvdssub  16046  gcdcllem1  16134  dfgcd2  16182  algcvg  16209  algcvga  16212  algfx  16213  lcmgcdlem  16239  lcmdvds  16241  lcmf  16266  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem  16274  lcmfdvds  16275  lcmfun  16278  coprmgcdb  16282  coprmdvds1  16285  coprmdvds2  16287  coprmprod  16294  coprmproddvds  16296  prmind2  16318  dvdsprime  16320  nprm  16321  dvdsprm  16336  exprmfct  16337  coprm  16344  isprm6  16347  prmfac1  16354  eulerthlem2  16411  pcqmul  16482  pcqcl  16485  pc2dvds  16508  pcz  16510  prmpwdvds  16533  infpn2  16542  vdwlem12  16621  ramub2  16643  rami  16644  ramcl  16658  prmdvdsprmop  16672  prmlem0  16735  mreintcl  17221  ismred2  17229  mrissmrcd  17266  mreexexlemd  17270  iscatd2  17307  moni  17365  yoniso  17919  isprs  17930  prslem  17931  drsdirfi  17938  ispos  17947  posi  17950  isposd  17956  pospropd  17960  lubfval  17983  lublecllem  17993  glbfval  17996  joinle  18019  meetle  18033  poslubmo  18044  posglbmo  18045  lubl  18145  lubun  18148  clatleglb  18151  ipodrsima  18174  acsdrsel  18176  isacs4lem  18177  isacs5lem  18178  acsdrscl  18179  mreclatBAD  18196  pslem  18205  dirtr  18235  mndind  18381  mhmlem  18610  isnsg2  18699  ghmf1  18778  orbsta  18834  symgextf1  18944  gsmsymgrfix  18951  gsmsymgreq  18955  symggen  18993  psgnunilem4  19020  sylow1lem1  19118  sylow2alem2  19138  sylow2a  19139  lsmmod  19196  lsmdisj2  19203  efgsrel  19255  efgredlemd  19265  efgredlem  19268  efgred  19269  gsumzaddlem  19437  gsummptnn0fz  19502  gsummptnn0fzfv  19503  telgsumfzs  19505  telgsums  19509  dprdval  19521  dprddisj2  19557  ablfac1eulem  19590  pgpfac1lem1  19592  pgpfac1lem5  19597  pgpfac1  19598  pgpfaclem2  19600  pgpfac  19602  irredmul  19866  f1rhm0to0ALT  19900  isdrngrd  19932  sdrgacs  19984  islbs3  20332  rrgval  20471  rrgeq0i  20473  isdomn  20478  domneq0  20481  prmirredlem  20606  znfld  20680  znrrg  20685  cygznlem3  20689  isphl  20745  ipeq0  20755  isphld  20771  phlpropd  20772  lsmcss  20809  frlmphl  20898  frlmup1  20915  lindfrn  20938  islindf4  20955  islindf5  20956  mplsubglem  21115  mpllsslem  21116  mplcoe1  21148  mplcoe5  21151  mpfind  21227  ismhp3  21243  coe1fzgsumd  21383  gsummoncoe1  21385  pf1ind  21431  evl1gsumd  21433  dmatelnd  21553  mat1scmat  21596  mdetdiaglem  21655  mdetralt  21665  mdetralt2  21666  mdetunilem1  21669  mdetunilem2  21670  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  smadiadetr  21732  pmatcoe1fsupp  21758  mp2pm2mplem4  21866  uniopn  21954  fiinopn  21958  epttop  22067  clsndisj  22134  elcls3  22142  neiptoptop  22190  neiptopnei  22191  cnpval  22295  iscnp  22296  cnpimaex  22315  lmcvg  22321  cnprest  22348  cnprest2  22349  lmss  22357  lmff  22360  t0sep  22383  hausnei  22387  isnrm2  22417  t1sep2  22428  isreg2  22436  iscmp  22447  cmpcov  22448  cmpsublem  22458  cmpsub  22459  tgcmp  22460  uncmp  22462  fiuncmp  22463  hauscmplem  22465  cmpfi  22467  cmpfii  22468  dfconn2  22478  connsuba  22479  connsub  22480  nconnsubb  22482  1stcclb  22503  1stcfb  22504  2ndc1stc  22510  1stcrest  22512  1stcelcls  22520  restnlly  22541  lly1stc  22555  comppfsc  22591  kgenval  22594  kgeni  22596  kgencn2  22616  ptcldmpt  22673  ptclsg  22674  dfac14lem  22676  dfac14  22677  txcnp  22679  ptcnp  22681  hausdiag  22704  txlm  22707  tx1stc  22709  xkococn  22719  cnmpt12  22726  cnmpt22  22733  kqt0lem  22795  isr0  22796  regr1lem2  22799  kqreglem1  22800  r0sep  22807  ptcmpfi  22872  elmptrab  22886  isfil  22906  filss  22912  isufil2  22967  cfinufil  22987  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  flimopn  23034  flimrest  23042  flftg  23055  cnpflf  23060  txflf  23065  fclsopni  23074  fclsrest  23083  fclscf  23084  flimfnfcls  23087  fcfnei  23094  alexsublem  23103  alexsubb  23105  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  cnextcn  23126  cnextfres1  23127  tgpt0  23178  qustgplem  23180  tsmsi  23193  tsmssubm  23202  tsmsres  23203  tsmsf1o  23204  tsmsxp  23214  ustssel  23265  ust0  23279  ustuqtop4  23304  ucnima  23341  ucncn  23345  iscusp  23359  cuspcvg  23361  imasdsf1olem  23434  blssps  23485  blss  23486  metss  23570  comet  23575  metcnp3  23602  metcnp2  23604  txmetcnp  23609  metuel2  23627  metucn  23633  nrmmetd  23636  nlmvscn  23757  nrginvrcn  23762  nmolb  23787  xrge0tsms  23903  divcn  23937  fsumcn  23939  elcncf2  23959  cncfi  23963  mulc1cncf  23974  cncfmet  23978  xrhmeo  24015  bndth  24027  nmoleub2lem2  24185  nmoleub3  24188  ipcn  24315  lmmbr  24327  caucfil  24352  pmltpc  24519  ovolfiniun  24570  ovolicc2lem3  24588  ovolicc2  24591  mblsplit  24601  finiunmbl  24613  volfiniun  24616  voliunlem3  24621  ioorinv  24645  ioorcl  24646  dyadmax  24667  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  volcn  24675  vitalilem2  24678  vitalilem3  24679  vitali  24682  i1fd  24750  itg2seq  24812  itg2addlem  24828  itgfsum  24896  ellimc3  24948  dvbsss  24971  dvnres  25000  dvmptfsum  25044  dvferm1lem  25053  dvferm2lem  25055  rolle  25059  c1lip1  25066  lhop1lem  25082  lhop1  25083  dvfsumlem2  25096  dvfsumlem4  25098  dvfsumrlim  25100  dvfsum2  25103  ftc1a  25106  ftc1lem6  25110  mdegleb  25134  mdeglt  25135  deg1leb  25165  deg1lt  25167  ply1divex  25206  fta1glem2  25236  fta1g  25237  plyco0  25258  plyeq0lem  25276  coeeq2  25308  dgrle  25309  dgrcolem2  25340  dgrco  25341  plydivlem4  25361  plydivex  25362  fta1lem  25372  fta1  25373  vieta1lem2  25376  vieta1  25377  aalioulem2  25398  aalioulem4  25400  abelth  25505  cxpcn3  25806  rlimcnp  26020  xrlimcnp  26023  cxploglim  26032  scvxcvx  26040  jensen  26043  lgamgulmlem2  26084  wilthlem2  26123  wilthlem3  26124  fta  26134  dvdsmulf1o  26248  perfectlem2  26283  dchrelbas3  26291  dchrelbas4  26296  dchrn0  26303  bcmono  26330  lgsdir2lem4  26381  lgsdchr  26408  gausslemma2dlem0i  26417  lgseisenlem2  26429  lgsquad2lem2  26438  2sqlem6  26476  2sqlem8  26479  2sqlem10  26481  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  istrkgb  26720  istrkgcb  26721  istrkge  26722  axtgcgrid  26728  axtg5seg  26730  axtgbtwnid  26731  axtgpasch  26732  axtgcont1  26733  axtgeucl  26737  iscgrglt  26779  tgcgr4  26796  axcgrtr  27186  gropd  27304  grstructd  27305  upgredg2vtx  27414  upgredgpr  27415  edglnl  27416  numedglnl  27417  usgredg2vtxeuALT  27492  nbgr2vtx1edg  27620  finsumvtxdg2size  27820  wlkp1lem8  27950  upgrwlkdvdelem  28005  usgr2wlkneq  28025  usgr2pthlem  28032  pthdlem2lem  28036  uspgrn2crct  28074  2pthdlem1  28196  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  3pthdlem1  28429  eupth2  28504  frgr3vlem1  28538  3vfriswmgrlem  28542  frgrwopreglem4a  28575  frgr2wwlk1  28594  wlkl0  28632  numclwlk2lem2f1o  28644  friendshipgt3  28663  eulplig  28748  nvz  28932  nmobndseqi  29042  nmobndseqiALT  29043  nmlno0  29058  blocnilem  29067  dipdir  29105  dipass  29108  siilem2  29115  ubthlem2  29134  ubth  29136  htth  29181  normpyth  29408  norm3lemt  29415  chlimi  29497  chcompl  29505  omlsii  29666  pjoml  29699  h1de2i  29816  elspansn2  29830  h1datom  29845  pjoml2  29874  pjoml3  29875  lecm  29880  chscllem2  29901  osum  29908  spansncv  29916  pjcjt2  29955  pjopyth  29983  eigre  30098  eigorth  30101  hhcno  30167  hhcnf  30168  cnopc  30176  cnfnc  30193  nmcexi  30289  nmcopexi  30290  nmcfnexi  30314  pjssge0i  30429  hstel2  30482  stj  30498  stri  30520  hstri  30528  stcltr1i  30537  mdbr  30557  mdi  30558  mdbr3  30560  mdbr4  30561  dmdbr  30562  dmdmd  30563  dmdi  30565  dmdbr3  30568  dmdbr4  30569  dmdbr5  30571  mdsl1i  30584  mdslmd1lem3  30590  mdslmd1lem4  30591  mdslmd1i  30592  csmdsymi  30597  cvmd  30599  atss  30609  atom1d  30616  chcv1  30618  hatomic  30623  atord  30651  atcvat2  30652  mddmdin0i  30694  opreu2reuALT  30726  rmoxfrd  30742  ifeqeqx  30786  ssiun2sf  30800  iinabrex  30809  ssrelf  30856  fmptcof2  30896  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1lem  30901  suppovss  30919  fz1nntr  31027  nn0min  31036  fsumiunle  31045  wrdt2ind  31127  ressprs  31143  resspos  31146  toslublem  31152  tosglblem  31154  mntoval  31162  ismntd  31164  dfmgc2lem  31175  dfmgc2  31176  xrge0tsmsd  31219  isomnd  31229  omndadd  31234  gsumle  31252  fzto1st  31272  psgnfzto1st  31274  submarchi  31342  archirng  31344  archiexdiv  31346  archiabllem1a  31347  archiabllem2a  31350  archiabl  31354  gsumvsca1  31381  gsumvsca2  31382  isorng  31400  orngmul  31404  isarchiofld  31418  linds2eq  31477  isprmidl  31515  prmidl  31517  prmidlc  31526  ismxidl  31536  mxidlmax  31539  rprmval  31566  isrprm  31567  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  submateq  31661  lmatfval  31666  lmatcl  31668  iscref  31696  crefi  31699  pcmplfin  31712  xrge0iifiso  31787  esumcvg  31954  esum2dlem  31960  sigaclcu  31985  sigaclci  32000  unelsiga  32002  unelldsys  32026  sigapildsys  32030  ldgenpisyslem1  32031  fiunelros  32042  measvun  32077  measiun  32086  carsgmon  32181  carsgsigalem  32182  carsgclctunlem2  32186  carsgclctun  32188  pmeasmono  32191  pmeasadd  32192  sibfof  32207  sitgclg  32209  eulerpartlemgvv  32243  signsply0  32430  signstfvneq0  32451  breprexp  32513  hgt749d  32529  istrkg2d  32546  axtgupdim2ALTV  32548  bnj1385  32712  bnj110  32738  bnj222  32763  bnj229  32764  bnj590  32790  bnj865  32803  bnj849  32805  bnj981  32830  bnj1014  32841  bnj1015  32842  bnj1112  32863  bnj1118  32864  bnj1123  32866  bnj1128  32870  bnj1125  32872  bnj1148  32876  bnj1154  32879  bnj1326  32906  bnj1384  32912  bnj1489  32936  bnj1497  32940  funen1cnv  32960  f1resfz0f1d  32972  cplgredgex  32982  acycgrcycl  33009  subfacp1lem6  33047  erdszelem9  33061  kur14lem9  33076  sconnpht  33091  cvmsss2  33136  cvmliftlem7  33153  cvmliftlem10  33156  fmlasuc  33248  gonar  33257  goalr  33259  mclsrcl  33423  mclsssvlem  33424  mclsval  33425  mclsax  33431  mclsind  33432  mclsppslem  33445  iota5f  33571  fununiq  33649  setinds  33660  dfon2lem3  33667  dfon2lem4  33668  dfon2lem5  33669  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  dfon2  33674  tfisg  33692  ttrclss  33706  ttrclselem2  33712  frpoins3xpg  33714  frpoins3xp3g  33715  poxp2  33717  frxp2  33718  xpord2ind  33721  poxp3  33723  frxp3  33724  xpord3ind  33727  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd2  33846  noinfcbv  33847  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem1  33853  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd2  33861  nocvxminlem  33899  madebdaylemold  34005  madebdaylemlrcut  34006  madebday  34007  lrrecpo  34025  btwnconn1lem11  34326  linethru  34382  fwddifnp1  34394  rankelg  34397  rankeq1o  34400  subtr  34430  subtr2  34431  trer  34432  nn0prpwlem  34438  nn0prpw  34439  neibastop2lem  34476  filnetlem4  34497  bj-hbxfrbi  34738  bj-hbyfrbi  34739  bj-ssblem1  34762  bj-ssblem2  34763  bj-ax12  34765  irrdiff  35424  relowlssretop  35461  rdgeqoa  35468  rdgssun  35476  exrecfnlem  35477  finxpreclem6  35494  pibp19  35512  pibt2  35515  wl-mo3t  35658  wl-sb8mot  35660  finixpnum  35689  matunitlindflem1  35700  ptrest  35703  poimirlem13  35717  poimirlem14  35718  poimirlem17  35721  poimirlem18  35722  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem28  35732  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  poimir  35737  heicant  35739  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  voliunnfl  35748  volsupnfl  35749  mbfresfi  35750  itg2addnclem3  35757  ftc1cnnc  35776  ftc1anclem7  35783  ftc1anc  35785  sdclem2  35827  fdc  35830  fdc1  35831  neificl  35838  mettrifi  35842  sstotbnd2  35859  cntotbnd  35881  heibor1lem  35894  bfp  35909  isass  35931  ismgmOLD  35935  isexid2  35940  iscringd  36083  ispridl  36119  pridl  36122  ismaxidl  36125  maxidlmax  36128  ispridlc  36155  pridlc  36156  dmnnzd  36160  relcnveq2  36385  ecin0  36411  elrelscnveq2  36538  elsymrels3  36595  eltrrels3  36621  eleqvrels3  36633  eqvrelqsel  36656  axc11n-16  36879  ax12eq  36882  ax12el  36883  ax12inda  36889  ax12v2-o  36890  fsumshftd  36893  riotasv2d  36898  lshpdisj  36928  lsmsatcv  36951  lsat0cv  36974  lcvexchlem4  36978  lcvexchlem5  36979  l1cvpat  36995  isopos  37121  oposlem  37123  isoml  37179  omllaw  37184  isatl  37240  atlex  37257  iscvlat  37264  cvlexch1  37269  glbconN  37318  hlsuprexch  37322  ps-1  37418  3atlem5  37428  psubspi  37688  llnexchb2  37810  elpcliN  37834  pclfinclN  37891  ldilval  38054  ltrnfset  38058  ltrnset  38059  ltrnu  38062  trlfset  38101  trlset  38102  trlval2  38104  cdleme25cv  38299  cdleme31so  38320  cdleme31fv  38331  cdlemefrs29bpre0  38337  cdleme32fva  38378  cdleme40v  38410  trlord  38510  cdlemkid3N  38874  cdlemkid4  38875  dihffval  39171  dihfval  39172  dihval  39173  lpolconN  39428  mapdordlem2  39578  hdmapfval  39768  hdmapval  39769  hdmapval2  39773  aks4d1p7  40019  sticksstones1  40030  sticksstones2  40031  sticksstones10  40039  sticksstones12a  40041  isdomn4  40100  fsuppind  40202  nnn1suc  40217  ismrcd1  40436  ismrcd2  40437  ismrc  40439  isnacs3  40448  nacsfix  40450  mzpcompact2  40490  fphpd  40554  fphpdo  40555  monotuz  40679  monotoddzzfi  40680  monotoddzz  40681  oddcomabszz  40682  zindbi  40684  setindtrs  40763  dford3lem2  40765  ttac  40774  dnnumch1  40785  fnwe2lem2  40792  aomclem3  40797  aomclem6  40800  aomclem8  40802  dfac11  40803  dfac21  40807  islssfg2  40812  hbtlem5  40869  hbt  40871  flcidc  40915  mendlmod  40934  rababg  41070  elmapintrab  41073  iunrelexpuztr  41216  frege92  41452  frege104  41464  ntrkbimka  41537  ntrk0kbimka  41538  neik0pk1imk0  41546  isotone1  41547  isotone2  41548  ntrclsiso  41566  ntrclskb  41568  ntrneiiso  41590  ntrneik3  41595  ntrneix3  41596  gneispacess2  41645  grur1cld  41739  scottabf  41747  ismnu  41768  mnuop23d  41773  mnuunid  41784  ismnushort  41808  dvgrat  41819  cvgdvgrat  41820  binomcxplemnotnn0  41863  pm14.122b  41930  sbiota1  41941  fnchoice  42461  fiiuncl  42502  iunincfi  42533  disjf1  42609  wessf1ornlem  42611  disjinfi  42620  axccdom  42651  dmrelrnrel  42654  axccd  42657  monoords  42726  fperiodmullem  42732  supxrgere  42762  supxrgelem  42766  supxrge  42767  xrlexaddrp  42781  infxr  42796  infleinf  42801  supxrleubrnmptf  42881  monoordxrv  42912  monoordxr  42913  monoord2xr  42915  fsummulc1f  43002  fsumnncl  43003  fsumf1of  43005  fsumreclf  43007  fsumlessf  43008  fsumsermpt  43010  fmul01  43011  fmulcl  43012  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  fprodexp  43025  fprodabs2  43026  fprodcnlem  43030  climmulf  43035  climexp  43036  climsuse  43039  climrecf  43040  climinff  43042  climaddf  43046  mullimc  43047  mullimcf  43054  limcperiod  43059  sumnnodd  43061  lptre2pt  43071  limsupre  43072  neglimc  43078  addlimc  43079  0ellimcdiv  43080  limclner  43082  climsubmpt  43091  climreclf  43095  climeldmeqmpt  43099  climfveqmpt  43102  fnlimfvre  43105  climfveqf  43111  climfveqmpt3  43113  climeldmeqf  43114  limsupref  43116  limsupbnd1f  43117  climeqf  43119  climeldmeqmpt3  43120  climinf2  43138  limsupubuz  43144  climinf2mpt  43145  climinfmpt  43146  limsupmnf  43152  limsupequz  43154  limsupre2  43156  limsupequzmptf  43162  limsupre3  43164  lmbr3  43178  cnrefiisp  43261  xlimxrre  43262  xlimmnfvlem1  43263  xlimpnfvlem1  43267  climxlim2lem  43276  cncfshift  43305  cncfperiod  43310  icccncfext  43318  fprodcncf  43331  fperdvper  43350  dvmptmulf  43368  dvnmptdivc  43369  dvnmul  43374  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  iblspltprt  43404  itgspltprt  43410  stoweidlem3  43434  stoweidlem4  43435  stoweidlem6  43437  stoweidlem8  43439  stoweidlem15  43446  stoweidlem16  43447  stoweidlem17  43448  stoweidlem19  43450  stoweidlem20  43451  stoweidlem22  43453  stoweidlem23  43454  stoweidlem26  43457  stoweidlem27  43458  stoweidlem30  43461  stoweidlem31  43462  stoweidlem32  43463  stoweidlem34  43465  stoweidlem35  43466  stoweidlem42  43473  stoweidlem43  43474  stoweidlem48  43479  stoweidlem50  43481  stoweidlem51  43482  stoweidlem57  43488  stoweidlem59  43490  stoweidlem62  43493  wallispilem3  43498  dirkercncflem2  43535  fourierdlem11  43549  fourierdlem12  43550  fourierdlem15  43553  fourierdlem16  43554  fourierdlem21  43559  fourierdlem34  43572  fourierdlem41  43579  fourierdlem42  43580  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem68  43605  fourierdlem71  43608  fourierdlem72  43609  fourierdlem73  43610  fourierdlem76  43613  fourierdlem79  43616  fourierdlem81  43618  fourierdlem83  43620  fourierdlem86  43623  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem94  43631  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  etransclem2  43667  etransclem46  43711  salunicl  43747  saluncl  43748  intsaluni  43758  dfsalgen2  43770  sge0f1o  43810  sge0lempt  43838  sge0iunmptlemfi  43841  sge0p1  43842  sge0fodjrnlem  43844  sge0iunmpt  43846  sge0ltfirpmpt2  43854  sge0isummpt2  43860  sge0xaddlem2  43862  sge0xadd  43863  nnfoctbdjlem  43883  meadjuni  43885  meadjiun  43894  voliunsge0lem  43900  meaiuninclem  43908  meaiunincf  43911  meaiuninc3v  43912  meaiuninc3  43913  meaiininclem  43914  meaiininc  43915  omeunile  43933  isomenndlem  43958  ovn0lem  43993  ovnsubaddlem1  43998  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvle  44028  hspmbllem2  44055  hoimbl2  44093  vonhoire  44100  vonicclem2  44112  vonn0ioo2  44118  vonn0icc2  44120  salpreimagelt  44132  salpreimalegt  44134  pimdecfgtioc  44139  pimincfltioc  44140  pimincfltioo  44142  salpreimagtge  44148  salpreimaltle  44149  salpreimagtlt  44153  incsmf  44165  decsmf  44189  smflimlem1  44193  smflimlem2  44194  smflimlem3  44195  smflimlem4  44196  smfpimcclem  44227  funressnmo  44427  fcoresf1  44450  aiota0def  44475  euoreqb  44488  2reu8i  44492  2reuimp0  44493  funressndmafv2rn  44602  funressnbrafv2  44623  funbrafv2  44626  smonoord  44711  elsetpreimafvbi  44731  iccpartgt  44767  iccelpart  44773  iccpartiun  44774  icceuelpartlem  44775  icceuelpart  44776  iccpartnel  44778  fargshiftf1  44781  ichexmpl2  44810  ichnreuop  44812  ichreuopeq  44813  sprsymrelfolem2  44833  prproropf1olem4  44846  paireqne  44851  reupr  44862  reuopreuprim  44866  fmtnofac2  44909  fmtnofac1  44910  prmdvdsfmtnof1lem2  44925  perfectALTVlem2  45062  nfermltl8rev  45082  nfermltl2rev  45083  sbgoldbwt  45117  sbgoldbst  45118  sgoldbeven3prm  45123  sbgoldbm  45124  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  evengpop3  45138  evengpoap3  45139  bgoldbnnsum3prm  45144  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgblthelfgott  45155  tgoldbach  45157  isomuspgrlem2b  45169  ply1mulgsumlem2  45616  islininds  45675  linindslinci  45677  lindslinindsimp1  45686  linds0  45694  lindsrng01  45697  snlindsntorlem  45699  snlindsntor  45700  ldepsnlinc  45737  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855  nn0sumshdiglem2  45856  nn0sumshdig  45857  itschlc0yqe  45994  f1mo  46068  iscnrm3lem5  46119  iscnrm3r  46130  isprsd  46137  lubeldm2d  46140  glbeldm2d  46141  joindm2  46150  meetdm2  46152  ipolublem  46160  ipolub  46162  ipoglblem  46163  ipoglb  46165  functhinclem2  46211  fullthinc  46215  fullthinc2  46216  bnd2d  46273  setrec1lem1  46279  setrec1lem4  46282  setrec2fun  46284