MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylibr Unicode version

Theorem sylibr 203
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
sylibr.1  |-  ( ph  ->  ps )
sylibr.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
sylibr  |-  ( ph  ->  ch )

Proof of Theorem sylibr
StepHypRef Expression
1 sylibr.1 . 2  |-  ( ph  ->  ps )
2 sylibr.2 . . 3  |-  ( ch  <->  ps )
32biimpri 197 . 2  |-  ( ps 
->  ch )
41, 3syl 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  pm5.74rd  239  bitri  240  3imtr4i  257  con2bid  319  sylanbrc  645  oplem1  930  3mix1  1124  3mix2  1125  3jca  1132  syl3anbrc  1136  inegd  1323  cad11  1389  had1  1392  nfxfrd  1558  19.29r  1584  nfdv  1620  19.8w  1660  19.39  1673  19.24  1674  19.34  1675  19.8a  1720  spimeh  1724  hbim1  1734  nfd  1748  nfim1  1823  nfan1  1824  ax12olem2  1871  spime  1919  sbn  2001  spsbe  2014  ax11eq  2133  ax11el  2134  mo  2166  eu2  2169  exmo  2189  2exeu  2221  2mo  2222  2eu6  2229  bm1.1  2269  eqrdv  2282  3eltr4g  2367  abbi2dv  2399  abbi1dv  2400  nfcd  2415  nfcxfrd  2418  3netr4g  2476  necon3ai  2487  alral  2602  rspe  2605  rsp2e  2607  rgen2a  2610  ralrimi  2625  r19.27av  2682  mormo  2753  nrexrmo  2758  cgsex2g  2821  cgsex4g  2822  spc2egv  2871  spc3egv  2873  rspce  2880  ceqex  2899  mo2icl  2945  reu3  2956  reu6i  2957  sbc5  3016  rspesbca  3072  rmo2i  3078  sbnfc2  3142  ssrdv  3186  3sstr4g  3220  syl5eqss  3223  ss2abdv  3247  abssdv  3248  rabssdv  3254  ss2rabdv  3255  ssun1  3339  unssad  3353  unssbd  3354  uneqin  3421  reuss2  3449  ne0i  3462  reximdva0  3467  minel  3511  uneqdifeq  3543  disjsn2  3695  absneu  3702  rabsneu  3703  elunii  3833  dfnfc2  3846  uniss2  3859  unidif  3860  ssunieq  3861  intab  3893  iunss2  3948  iunxdif2  3951  riinrab  3978  invdisj  4013  disjiun  4014  disjxiun  4021  3brtr4g  4056  trin  4124  triun  4127  truni  4128  trint  4129  iinexg  4174  class2seteq  4178  notzfaus  4184  pwuni  4205  snelpwi  4219  copsex2t  4252  euotd  4266  opthwiener  4267  ispod  4321  sotric  4339  isso2i  4345  somo  4347  exse  4356  frc  4358  fr2nr  4370  epfrc  4378  trssord  4408  ordelord  4413  ordtri1  4424  orddisj  4429  suctr  4474  trsuc2OLD  4476  eusvnf  4528  eusvnfb  4529  eusv2nf  4531  reusv6OLD  4544  ralxfr2d  4549  rabxfrd  4554  reuhypd  4560  eldifpw  4565  elpwun  4566  elpwunsn  4567  iunpw  4569  fr3nr  4570  ordon  4573  ssorduni  4576  ssonprc  4582  onint0  4586  onminex  4597  suceloni  4603  ordsucss  4608  ordsucelsuc  4612  ordsucuniel  4614  nlimsucg  4632  ordunisuc2  4634  ordzsl  4635  tfi  4643  peano5  4678  eqrelrdv  4782  xpsspw  4796  xpsspwOLD  4797  relint  4808  relop  4833  opeldm  4881  elres  4989  relssres  4991  exse2  5046  issref  5055  trin2  5065  dminss  5094  imainss  5095  xpnz  5098  soex  5121  dmmptg  5168  relrelss  5194  cnviin  5210  funmo  5237  funco  5258  funun  5262  funprg  5267  funtp  5269  fununi  5282  funcnvuni  5283  funimaexg  5295  isarep2  5298  fnunsn  5317  2elresin  5321  fnimadisj  5330  fco  5364  funssxp  5368  fssres  5374  feu  5383  fimacnvdisj  5385  fabexg  5388  f00  5392  f1co  5412  fores  5426  foco  5427  foconst  5428  f1ores  5453  foimacnv  5456  f1oun  5458  fun11iun  5459  f1oco  5462  fo00  5475  fv3  5502  tz6.12-1  5505  nfunsn  5520  dffv2  5554  funfvbrb  5600  respreima  5616  iinpreima  5617  fvelrn  5623  dff2  5634  dff3  5635  dffo4  5638  exfo  5640  ffvresb  5652  fsn  5658  fpr  5666  fsnunf  5680  fsnunfv  5682  zfrep6  5710  elabrex  5727  dff1o6  5753  foeqcnvco  5766  fveqf1o  5768  fliftel1  5771  soisoi  5787  isocnv3  5791  isores1  5793  isoini2  5798  wemoiso  5817  wemoiso2  5818  knatar  5819  eloprabga  5896  fnoprabg  5907  oprabexd  5922  ndmovass  5970  ndmovdistr  5971  fo1stres  6105  fo2ndres  6106  unielxp  6120  1st2ndbr  6131  fmpt2co  6164  1stconst  6169  2ndconst  6170  curry1  6172  cnvf1olem  6178  frxp  6187  poxp  6189  soxp  6190  fnse  6194  reldmtpos  6204  tposfun  6212  dftpos4  6215  sorpssi  6245  sorpssuni  6248  sorpssint  6249  sorpsscmpl  6250  sniota  6280  pwuninel  6296  undefnel  6299  riotasbc  6316  onfununi  6354  onnseq  6357  smores  6365  smores2  6367  smogt  6380  tfrlem9a  6398  tfrlem10  6399  tfr3  6411  tz7.48lem  6449  tz7.48-1  6451  tz7.49  6453  tz7.49c  6454  seqomlem2  6459  seqomlem4  6461  abianfp  6467  2oconcl  6498  oawordeulem  6548  oalimcl  6554  oacomf1o  6559  omlimcl  6572  omeulem1  6576  oeordi  6581  oelim2  6589  oeeulem  6595  oaabslem  6637  oaabs2  6639  omabslem  6640  omabs  6641  brdifun  6683  swoso  6687  ecelqsdm  6725  iiner  6727  qsdisj2  6733  eroveu  6749  erovlem  6750  ecopovtrn  6757  th3qlem1  6760  pmsspw  6798  map0b  6802  mapsn  6805  mapsncnv  6810  ixpf  6834  uniixp  6835  ixpexg  6836  resixp  6847  relsdom  6866  f1oen3g  6873  ssdomg  6903  domtr  6910  domdifsn  6941  omxpenlem  6959  omf1o  6961  sbthlem2  6968  sbthlem3  6969  sbthlem7  6973  sbthlem8  6974  sdomdif  7005  2pwuninel  7012  2pwne  7013  domss2  7016  xpf1o  7019  xpmapenlem  7024  mapdom2  7028  limenpsi  7032  infensuc  7035  php3  7043  1sdom  7061  ominf  7071  isinf  7072  fineqvlem  7073  pssnn  7077  ssnnfi  7078  ssfi  7079  xpfir  7081  dif1enOLD  7086  dif1en  7087  findcard  7093  findcard2  7094  findcard3  7096  ac6sfi  7097  frfi  7098  unblem1  7105  unblem2  7106  nnsdomg  7112  unfi  7120  domunfican  7125  fodomfi  7131  unifi2  7142  pwfilem  7146  pwfi  7147  fissuni  7156  fipreima  7157  finsschain  7158  indexfi  7159  fival  7162  fiin  7171  dffi2  7172  fisn  7176  dffi3  7180  marypha1lem  7182  supmo  7199  suppr  7215  ordtypelem2  7230  ordtypelem3  7231  ordtypelem9  7237  hartogslem1  7253  wemapso2lem  7261  wemapso2  7263  card2inf  7265  wdom2d  7290  wdomd  7291  xpwdomg  7295  ixpiunwdom  7301  inf3lem3  7327  inf3lem6  7330  infdifsn  7353  cantnfle  7368  cantnflt  7369  cantnff  7371  cantnfp1lem2  7377  cantnfp1lem3  7378  oemapvali  7382  cantnflem1a  7383  cantnflem1b  7384  cantnflem1c  7385  cantnflem1  7387  cantnf  7391  wemapwe  7396  oef1o  7397  cnfcom2lem  7400  cnfcom2  7401  cnfcom3lem  7402  cnfcom3  7403  trcl  7406  setind  7415  tcmin  7422  r1ordg  7446  r1pwss  7452  r1val1  7454  tz9.12lem1  7455  tz9.12lem3  7457  tz9.13  7459  r1elwf  7464  rankdmr1  7469  pwwf  7475  unwf  7478  uniwf  7487  rankr1c  7489  rankpwi  7491  rankval3b  7494  rankonidlem  7496  r1pw  7513  r1pwOLD  7514  r1pwcl  7515  rankuni2b  7521  rankelun  7540  rankelpr  7541  rankelop  7542  rankxplim3  7547  rankxpsuc  7548  tcwf  7549  tcrank  7550  scottex  7551  scott0  7552  hta  7563  cardf2  7572  isnumi  7575  tskwe  7579  cardid2  7582  carden2b  7596  cardsn  7598  cardprclem  7608  harval2  7626  dif1card  7634  r0weon  7636  infxpenlem  7637  infxpenc  7641  fseqdom  7649  dfac8clem  7655  ac5num  7659  ondomen  7660  acni2  7669  finacn  7673  acndom2  7677  infpwfien  7685  alephnbtwn  7694  alephsucdom  7702  infenaleph  7714  dfac5lem4  7749  dfac5  7751  dfac2a  7752  dfac2  7753  dfac9  7758  dfacacn  7763  dfac13  7764  dfac12lem2  7766  kmlem4  7775  kmlem6  7777  kmlem8  7779  kmlem13  7784  cda1en  7797  cdainflem  7813  pwsdompw  7826  infdif  7831  infmap2  7840  ackbij1lem18  7859  cff  7870  cflm  7872  cardcf  7874  cfsuc  7879  cff1  7880  cfflb  7881  cflim3  7884  cflim2  7885  cfss  7887  cfslb  7888  cofsmo  7891  cfsmolem  7892  coftr  7895  isfin3  7918  fin23lem7  7938  enfin2i  7943  fin23lem26  7947  fin23lem30  7964  fin23lem32  7966  fin23lem38  7971  fin23lem40  7973  fin23lem41  7974  isf32lem2  7976  isf32lem3  7977  compsscnvlem  7992  compssiso  7996  isf34lem5  8000  isf34lem7  8001  isf34lem6  8002  isfin1-2  8007  isfin1-3  8008  fin56  8015  fin1a2lem11  8032  fin1a2lem13  8034  fin1a2s  8036  hsmexlem2  8049  domtriomlem  8064  dcomex  8069  axdc2lem  8070  axdc3lem  8072  axdc3lem2  8073  axdc3lem4  8075  axdc4lem  8077  axcclem  8079  ac6c4  8104  ac9  8106  ac9s  8116  zorn2lem6  8124  zorn2lem7  8125  zorng  8127  ttukeylem1  8132  ttukeylem6  8137  ttukeylem7  8138  axdclem  8142  brdom3  8149  brdom5  8150  brdom4  8151  iunfo  8157  iundom2g  8158  entric  8175  entri2  8176  ondomon  8181  ficard  8183  konigthlem  8186  alephval2  8190  pwcfsdom  8201  fpwwe2lem1  8249  fpwwe2lem12  8259  fpwwe2lem13  8260  fpwwe2  8261  fpwwe  8264  canthnumlem  8266  canthwelem  8268  canthwe  8269  canthp1lem2  8271  pwfseqlem1  8276  pwfseqlem3  8278  pwfseqlem4a  8279  pwfseqlem4  8280  pwfseqlem5  8281  gchac  8291  hargch  8295  alephgch  8296  gch2  8297  gch3  8298  wunfi  8339  intwun  8353  wunex2  8356  wuncval  8360  wunccl  8362  wuncval2  8365  tsksuc  8380  tskwe2  8391  inttsk  8392  inar1  8393  tskuni  8401  ingru  8433  gruina  8436  grur1a  8437  grur1  8438  axgroth3  8449  inaprc  8454  tskmcl  8459  nqerf  8550  recmulnq  8584  dmrecnq  8588  genpn0  8623  genpnnp  8625  genpcl  8628  nqpr  8634  psslinpr  8651  prlem934  8653  ltexprlem1  8656  ltexprlem4  8659  ltexprlem5  8660  ltexprlem7  8662  reclem2pr  8668  reclem3pr  8669  suplem1pr  8672  supexpr  8674  supsrlem  8729  supsr  8730  axaddrcl  8770  axmulrcl  8772  axrnegex  8780  axcnre  8782  axpre-lttrn  8784  wuncn  8788  cnegex  8989  recextlem2  9395  mulnzcnopr  9410  rereccl  9474  lbreu  9700  supmul1  9715  supmullem2  9717  supmul  9718  infmsup  9728  infmrgelb  9730  infmrlb  9731  nnm1nn0  10001  elnnnn0c  10005  nnnegz  10023  elnnz1  10045  zaddcl  10055  uzind  10099  eluz2b2  10286  zsupss  10303  uzwo3  10307  zmin  10308  znq  10316  qaddcl  10328  qmulcl  10330  qreccl  10332  irradd  10336  irrmul  10337  rpnnen1lem1  10338  rpnnen1lem2  10339  rpnnen1lem3  10340  rpnnen1lem5  10342  cnref1o  10345  qbtwnxr  10523  xrinfmss2  10625  elioo4g  10707  difreicc  10763  fzosplit  10895  elfzo0  10900  1mod  10992  fzennn  11026  fseqsupcl  11035  seqf2  11061  seqf1olem1  11081  seqid3  11086  seqz  11090  ser0f  11095  seqof  11099  expcl2lem  11111  1exp  11127  hashkf  11335  hashsng  11352  hashmap  11383  hashbclem  11386  hashbc  11387  hashf1lem1  11389  hashf1lem2  11390  iswrdi  11413  s1cl  11437  cats1un  11472  shftfval  11561  rennim  11720  cnpart  11721  sqrmo  11733  sqrneglem  11748  rexanuz  11825  sqreulem  11839  eqsqrd  11847  limsupgord  11942  limsupval2  11950  limsupgre  11951  rlimi  11983  climeu  12025  lo1res  12029  rlimmptrcl  12077  o1of2  12082  o1rlimmul  12088  lo1mptrcl  12091  o1mptrcl  12092  isercolllem3  12136  isercoll2  12138  caucvgrlem  12141  summolem3  12183  summo  12186  fsumss  12194  fsumsplit  12208  sumsn  12209  sumsplit  12227  fsum2dlem  12229  fsumcom2  12233  fsum0diag2  12241  fsum00  12252  fsumabs  12255  fsumrlim  12265  fsumo1  12266  o1fsum  12267  fsumiun  12275  fsumiunOLD  12277  hashiunOLD  12278  incexclem  12291  isumsup2  12301  isumltss  12303  infcvgaux2i  12312  mertenslem1  12336  mertenslem2  12337  ef0lem  12356  efcvgfsum  12363  tanval  12404  rpnnen2lem11  12499  rpnnen2  12500  ruclem6  12509  dvdslelem  12569  dvdsfac  12579  divalglem8  12595  bitsfzolem  12621  bitsinv1  12629  bitsinvp1  12636  sadfval  12639  sadcf  12640  smufval  12664  smupf  12665  smuval2  12669  smupvallem  12670  smu01lem  12672  smumullem  12679  gcdcllem3  12688  gcdaddmlem  12703  bezoutlem2  12714  algrf  12739  algcvgblem  12743  isprm2  12762  isprm3  12763  qredeu  12782  isprm5  12787  phicl2  12832  phibndlem  12834  phibnd  12835  dfphi2  12838  hashdvds  12839  phiprmpw  12840  phimullem  12843  odzcllem  12853  odzdvds  12856  pcdvdsb  12917  infpn2  12956  prmreclem1  12959  prmreclem2  12960  prmreclem3  12961  prmreclem4  12962  prmreclem5  12963  prmreclem6  12964  1arith  12970  4sqlem3  12993  4sqlem11  12998  4sqlem19  13006  vdwapf  13015  vdwlem6  13029  vdwlem8  13031  vdwlem9  13032  vdwlem13  13036  vdwnn  13041  ramtlecl  13043  0ram  13063  ram0  13065  ramub1lem1  13069  ramub1lem2  13070  ramub1  13071  setscom  13172  setsid  13183  restsspw  13332  prdshom  13362  imasaddfnlem  13426  imasaddvallem  13427  imasaddflem  13428  imasvscafn  13435  imasvscaf  13437  xpscfn  13457  xpsc0  13458  xpsc1  13459  mremre  13502  mrcuni  13519  submrc  13526  mreexexlem2d  13543  mreexexlem3d  13544  mreexexd  13546  isacs2  13551  isacs1i  13555  mreacs  13556  acsfn  13557  catideu  13573  isssc  13693  isfuncd  13735  funcoppc  13745  idfucl  13751  cofucl  13758  funcres2b  13767  wunfunc  13769  fthoppc  13793  idffth  13803  ressffth  13808  natixp  13822  nati  13825  fuccocl  13834  fucidcl  13835  invfuc  13844  homaf  13858  coapm  13899  setcepi  13916  catciso  13935  evlfcl  13992  curf2cl  14001  uncfcurf  14009  yonedalem4c  14047  yonedalem3b  14049  yonedalem3  14050  yonedainv  14051  drsdirfi  14068  isdrs2  14069  isposd  14085  lubprop  14110  glbprop  14115  isglbd  14217  odupos  14235  poslubmo  14246  ipoval  14253  ipolerval  14255  isacs4lem  14267  isacs5lem  14268  isacs4  14272  isacs3  14273  acsfiindd  14276  acsmapd  14277  mrelatglb  14283  mrelatlub  14285  spwmo  14331  spweu  14332  mhmeql  14437  gsumvallem1  14444  gsumws1  14458  gsumwspan  14464  grpinveu  14512  prdsinvlem  14599  subgint  14637  0subg  14638  cycsubg  14641  subgacs  14648  nsgacs  14649  0nsg  14658  eqgfval  14661  ghmeql  14701  gimco  14728  brgici  14730  gass  14751  symgval  14767  cayley  14785  oppgsubm  14831  oppgsubg  14832  odcl  14847  dfod2  14873  odf1o2  14880  gexcl  14887  gex1  14898  pgpfi1  14902  sylow1lem2  14906  sylow1lem3  14907  odcau  14911  pgpssslw  14921  sylow2alem2  14925  sylow2a  14926  sylow2blem1  14927  sylow2blem3  14929  sylow3lem3  14936  sylow3lem6  14939  pj1fval  14999  efgrcl  15020  efgval  15022  efgi  15024  efgi2  15030  efgsval2  15038  efgs1  15040  efgs1b  15041  efgsp1  15042  efgsres  15043  efgsfo  15044  efgredlemd  15049  efgredlem  15052  efgrelexlemb  15055  0frgp  15084  iscmnd  15097  gexex  15141  frgpnabllem1  15157  iscygodd  15171  prmcyg  15176  lt6abl  15177  gsumval3eu  15186  gsumval3  15187  gsumzaddlem  15199  gsumzsplit  15202  gsummhm2  15208  gsumunsn  15217  gsumpt  15218  gsum2d  15219  gsumcom2  15222  eldprd  15235  dprdfadd  15251  dprdspan  15258  dprdres  15259  dprdcntz2  15269  dprd2dlem2  15271  dprd2dlem1  15272  dprd2da  15273  dprd2d2  15275  dmdprdsplit2lem  15276  dpjfval  15286  ablfacrplem  15296  ablfacrp  15297  ablfacrp2  15298  ablfac1b  15301  ablfac1eulem  15303  ablfac1eu  15304  pgpfac1lem5  15310  pgpfaclem1  15312  ablfaclem2  15317  ablfaclem3  15318  ablfac2  15320  pws1  15395  opprrngb  15410  irredn0  15481  isdrngd  15533  isdrngrd  15534  opprsubrg  15562  subrgint  15563  subrgmre  15565  issubdrg  15566  issrngd  15622  lsssn0  15701  lss1d  15716  lssintcl  15717  lssmre  15719  lspf  15727  lspval  15728  lspextmo  15809  brlmici  15818  lsppratlem1  15896  lsppratlem6  15901  lbsextlem1  15907  lbsextlem2  15908  lbsextlem3  15909  lbsextlem4  15910  sraval  15925  rsp1  15972  drngnidl  15977  abvn0b  16039  fidomndrng  16044  aspval  16064  asplss  16065  aspid  16066  aspsubrg  16067  psrbagconcl  16115  psrbagconf1o  16116  psrass1lem  16119  psraddcl  16124  psrmulcllem  16128  psrvscacl  16134  psr0cl  16135  psrnegcl  16137  psr1cl  16143  subrgpsr  16159  mvrf  16165  mplmon  16203  mplcoe1  16205  mplcoe2  16207  opsrtoslem2  16222  subrgasclcl  16236  coe1fval3  16285  coe1z  16336  coe1mul2  16342  coe1tm  16345  prmirredlem  16442  mulgrhm2  16457  zlmlmod  16473  zlmassa  16474  znf1o  16501  znfi  16509  znidomb  16511  ipcl  16533  cssmre  16589  obselocv  16624  eltopspOLD  16652  istopon  16659  toponcom  16664  topgele  16668  topontopn  16676  tsettps  16677  tgval  16689  eltg2b  16693  en2top  16719  tgss2  16721  bastop2  16728  distop  16729  fctop  16737  cctop  16739  ppttop  16740  pptbas  16741  epttop  16742  cldss2  16763  clscld  16780  elcls  16806  mretopd  16825  toponmre  16826  neisspw  16840  neips  16846  neiuni  16855  clslp  16875  restbas  16885  resstps  16913  ordtbaslem  16914  ordtbas2  16917  ordtbas  16918  ordttopon  16919  ordtopn1  16920  ordtopn2  16921  ordtrest2  16930  iocpnfordt  16941  icomnfordt  16942  lecldbas  16945  tgcn  16978  tgcnp  16979  subbascn  16980  cnntr  17000  lmff  17025  t0dist  17049  pnrmopn  17067  lpcls  17088  t1sep  17094  dishaus  17106  ordthauslem  17107  cmpcovf  17114  discmp  17121  cmpsublem  17122  cmpsub  17123  fiuncmp  17127  hauscmplem  17129  cmpfi  17131  cnconn  17144  consubclo  17146  iuncon  17150  clscon  17152  concompid  17153  1stcfb  17167  2ndci  17170  2ndcsb  17171  2ndc1stc  17173  1stcrest  17175  2ndcctbss  17177  2ndcdisj  17178  2ndcomap  17180  2ndcsep  17181  dis2ndc  17182  nlly2i  17198  llynlly  17199  restnlly  17204  llyrest  17207  llyidm  17210  nllyidm  17211  hausllycmp  17216  cldllycmp  17217  lly1stc  17218  dislly  17219  llycmpkgen2  17241  1stckgenlem  17244  kgencn2  17248  txuni2  17256  txbasex  17257  txbas  17258  elptr  17264  elptr2  17265  ptbasin2  17269  ptbasfi  17272  xkoopn  17280  xkouni  17290  ptpjopn  17302  ptclsg  17305  dfac14  17308  xkoccn  17309  txcnp  17310  ptcnplem  17311  ptcnp  17312  txcnmpt  17314  txcn  17316  ptcn  17317  prdstopn  17318  txdis  17322  txindis  17324  txdis1cn  17325  txlly  17326  txnlly  17327  pthaus  17328  ptrescn  17329  txtube  17330  txcmplem1  17331  txcmplem2  17332  tx1stc  17340  xkohaus  17343  xkococnlem  17349  xkococn  17350  cnmpt11  17353  cnmpt1t  17355  cnmpt12  17357  cnmpt21  17361  cnmpt2t  17363  cnmpt22  17364  cnmptkp  17370  cnmptk1  17371  cnmpt1k  17372  cnmptkk  17373  cnmptk1p  17375  cnmptk2  17376  cnmpt2k  17378  txcon  17379  qtoptop2  17386  qtopuni  17389  basqtop  17398  tgqtop  17399  qtopeu  17403  imastps  17408  kqdisj  17419  kqcldsat  17420  kqt0  17433  kqreg  17438  kqnrm  17439  hmeofval  17445  hmphi  17464  hmphdis  17483  ordthmeolem  17488  xpstopnlem1  17496  ptcmpfi  17500  reghaus  17512  fbssfi  17528  fbssint  17529  opnfbas  17533  trfbas2  17534  isfil2  17547  snfil  17555  fsubbas  17558  fgcl  17569  neifil  17571  fbasrn  17575  filuni  17576  supfil  17586  uzrest  17588  uzfbas  17589  isufil2  17599  filssufilg  17602  numufl  17606  fixufil  17613  uffixsn  17616  rnelfmlem  17643  hausflimi  17671  flimsncls  17677  hauspwpwf1  17678  flftg  17687  txflf  17697  fclscmp  17721  alexsublem  17734  alexsub  17735  alexsubb  17736  alexsubALTlem2  17738  alexsubALTlem3  17739  alexsubALTlem4  17740  ptcmplem3  17744  ptcmplem4  17745  cnmpt1plusg  17766  cnmpt2plusg  17767  tmdgsum  17774  oppgtmd  17776  distgp  17778  indistgp  17779  symgtgp  17780  clssubg  17787  clsnsg  17788  cldsubg  17789  tgpconcompeqg  17790  tgpconcomp  17791  ghmcnp  17793  divstgplem  17799  tsmsfbas  17806  tsmsid  17818  tsmsf1o  17823  tgptsmscls  17828  tsmssplit  17830  tsmsxp  17833  cnmpt1vsca  17872  cnmpt2vsca  17873  prdsxmetlem  17928  imasdsf1olem  17933  blbas  17972  setsmstopn  18020  prdsbl  18033  blsscls2  18046  met1stc  18063  met2ndci  18064  prdsxmslem2  18071  tngtopn  18162  nrgtrg  18196  tgqioo  18302  zdis  18318  iccntr  18322  icccmplem1  18323  icccmplem2  18324  reconnlem1  18327  cnmpt1ds  18343  cnmpt2ds  18344  metdsf  18348  metnrmlem3  18361  fsumcn  18370  cncfmpt1f  18413  cncfmpt2ss  18415  cnmpt2pc  18422  icoopnst  18433  iocopnst  18434  cnllycmp  18450  evth  18453  lebnumlem1  18455  copco  18512  pcoass  18518  pi1xfrcnv  18551  zlmclm  18589  cnmpt1ip  18670  cnmpt2ip  18671  cfilres  18718  bcthlem5  18746  bcth  18747  minveclem1  18784  minveclem2  18786  minveclem3b  18788  minveclem4a  18790  pmltpc  18806  evthicc2  18816  ovolficcss  18825  ovolfsf  18827  ovolsf  18828  elovolmr  18831  ovolgelb  18835  ovolunlem1  18852  ovolfiniun  18856  ovoliunlem1  18857  ovoliunlem2  18858  ovoliun  18860  ovoliun2  18861  ovoliunnul  18862  ovolshftlem2  18865  ovolicc2lem4  18875  ovolicc2  18877  volfiniun  18900  iundisj  18901  voliunlem1  18903  voliunlem2  18904  voliunlem3  18905  volsup  18909  ovolioo  18921  ioorf  18924  uniioombllem3a  18935  uniioombllem3  18936  uniioombllem6  18939  dyadmax  18949  dyadmbllem  18950  dyadmbl  18951  opnmbllem  18952  volsup2  18956  vitalilem2  18960  vitalilem3  18961  vitalilem4  18962  vitalilem5  18963  vitali  18964  mbfconstlem  18980  mbfmptcl  18988  mbfeqalem  18993  mbfposr  19003  ismbf3d  19005  mbfinf  19016  mbflimsup  19017  mbflim  19019  i1fima2  19030  i1fd  19032  itg1val2  19035  i1fadd  19046  i1fmul  19047  itg1addlem4  19050  i1fmulc  19054  i1fposd  19058  itg1climres  19065  itg2lr  19081  itg2seq  19093  itg2mulc  19098  itg2splitlem  19099  itg2split  19100  itg2monolem1  19101  itg2i1fseq  19106  itg2gt0  19111  itg2cn  19114  iblcnlem  19139  itgss3  19165  itgfsum  19177  itgsplitioo  19188  itggt0  19192  limcvallem  19217  cnmptlimc  19236  limcco  19239  limciun  19240  dvfval  19243  perfdvf  19249  dvnfval  19267  dvcmul  19289  dvcobr  19291  dvmptcl  19304  dvmptco  19317  dvmptfsum  19318  dvcnvlem  19319  dveflem  19322  dvef  19323  dvferm1  19328  rolle  19333  c1liplem1  19339  dvlt0  19348  dvle  19350  dvne0  19354  lhop1lem  19356  dvfsumle  19364  dvfsumge  19365  dvfsumabs  19366  dvmptrecl  19367  dvfsumlem2  19370  itgparts  19390  itgsubstlem  19391  itgsubst  19392  evlseu  19396  mpfrcl  19398  evl1sca  19409  mpfind  19424  pf1rcl  19428  pf1ind  19434  deg1n0ima  19471  ply1divmo  19517  fta1blem  19550  ig1pcl  19557  elply2  19574  plyeq0lem  19588  plypf1  19590  coeeulem  19602  coeeq  19605  plycj  19654  plycpn  19665  vieta1lem1  19686  vieta1lem2  19687  plyexmo  19689  elqaalem1  19695  elqaalem3  19697  aannenlem1  19704  aaliou2  19716  taylfval  19734  taylf  19736  dvtaylp  19745  dvntaylp  19746  taylthlem1  19748  taylthlem2  19749  ulmcau  19768  ulmss  19770  ulmdvlem2  19774  mtest  19777  itgulm2  19781  radcnvlt1  19790  dvradcnv  19793  pserdvlem2  19800  abelthlem2  19804  abelthlem3  19805  sincn  19816  coscn  19817  reeff1o  19819  recosf1o  19893  dvlog  19994  efopn  20001  logtayl  20003  cxple2a  20042  cxpcn3  20084  cxpaddlelem  20087  cxpaddle  20088  ang180lem3  20105  logreclem  20112  isosctrlem2  20115  birthdaylem3  20244  xrlimcnp  20259  efrlim  20260  rlimcxp  20264  jensenlem1  20277  jensenlem2  20278  jensen  20279  fsumharmonic  20301  wilthlem2  20303  basellem9  20322  sgmss  20340  sgmnncl  20381  ppinprm  20386  chtprm  20387  chtnprm  20388  ppiltx  20411  mumul  20415  sqff1o  20416  musum  20427  dvdsmulf1o  20430  fsumdvdsmul  20431  fsumvma  20448  perfectlem2  20465  dchrelbas3  20473  dchrfi  20490  dchrptlem1  20499  dchrptlem2  20500  dchrptlem3  20501  dchrsum2  20503  bcmono  20512  bposlem4  20522  lgslem1  20531  lgsfcl2  20537  lgscllem  20538  lgsval2lem  20541  lgsdir2lem5  20562  lgsne0  20568  lgseisenlem2  20585  lgseisenlem3  20586  lgsquadlem2  20590  2sqlem2  20599  mul2sq  20600  2sqlem3  20601  2sqlem7  20605  2sqlem8  20607  2sqlem11  20610  2sqblem  20612  dchrisumlem3  20636  dchrisum0flblem1  20653  dchrisum0flb  20655  dchrisumn0  20666  pntlem3  20754  qrngdiv  20769  ex-br  20795  ex-natded9.26  20828  isgrpo  20857  grpofo  20860  grpoideu  20870  grpoinveu  20883  isgrpda  20958  ablomul  21016  ghgrp  21029  rngoideu  21045  rngmgmbs4  21078  rngomndo  21082  rngo1cl  21090  nmosetn0  21337  nmoolb  21343  nmlno0lem  21365  blocnilem  21376  blocni  21377  lnocni  21378  ubthlem1  21443  minvecolem1  21447  minvecolem2  21448  minvecolem5  21454  htthlem  21491  bcsiALT  21754  hlimadd  21768  shex  21787  hsn0elch  21823  hhsst  21839  hhsscms  21852  occon  21862  pjhthmo  21877  shscli  21892  choc0  21901  choc1  21902  shintcli  21904  spancl  21911  spanss  21923  ococin  21983  chsupsn  21988  pjoc1i  22006  chlejb1i  22051  chabs2  22092  spanuni  22119  spanunsni  22154  h1datomi  22156  cmbr3i  22175  cmbr4i  22176  lecmi  22177  chscllem2  22213  osumcor2i  22219  nonbooli  22226  pjss2i  22255  pjjsi  22275  pjmf1  22291  hmopex  22451  nmoplb  22483  nmfnlb  22500  nmlnop0iALT  22571  nmopun  22590  lnconi  22609  nmcfnlbi  22628  imaelshi  22634  cnlnadjlem3  22645  cnlnadjlem5  22647  cnlnadjeui  22653  cnlnssadj  22656  adjbdln  22659  adjbdlnb  22660  adjeq0  22667  branmfn  22681  hmopidmpji  22728  pjss2coi  22740  pjnormssi  22744  pjssdif2i  22750  pjinvari  22767  pjci  22776  pjcmul2i  22778  strlem1  22826  mdsl1i  22897  mdslmd3i  22908  csmdsymi  22910  mdexchi  22911  chpssati  22939  atomli  22958  chirredi  22970  mdsymlem6  22984  sumdmdii  22991  cmmdi  22992  sumdmdlem2  22995  dmdbr5ati  22998  dmdbr6ati  22999  dmdbr7ati  23000  cdjreui  23008  cdj3i  23017  nvof1o  23032  ballotlemfc0  23047  ballotlemfcc  23048  ballotlemiex  23056  ballotlemi1  23057  ballotlemii  23058  ballotlemsup  23059  ballotlemfrcn0  23084  subfacp1lem3  23120  subfacp1lem5  23122  subfacp1lem6  23123  erdszelem5  23133  erdszelem7  23135  erdszelem11  23139  kur14lem9  23152  pconcon  23169  txpcon  23170  conpcon  23173  cnllyscon  23183  iccllyscon  23188  rellyscon  23189  cvmcov  23201  cvmsss2  23212  cvmliftmo  23222  cvmlift2lem1  23240  cvmlift2lem12  23252  cvmlift2lem13  23253  cvmlift3lem2  23258  umgraex  23282  umgra1  23285  vdgr1d  23301  vdgr1b  23302  vdgr1a  23304  eupares  23306  eupap1  23307  eupath2lem3  23310  eupath2  23311  eupath  23312  vdegp1ai  23315  vdegp1bi  23316  ghomgrpilem2  23400  climuzcnv  23411  circum  23414  lediv2aALT  23420  relexpindlem  23443  rtrclreclem.trans  23450  rtrclreclem.min  23451  dfrtrcl2  23452  dedekind  23488  relin01  23495  fundmpss  23526  dfon2lem4  23546  dfon2lem5  23547  dfon2lem7  23549  dfon2lem9  23551  dfon2  23552  rdgprc  23555  elpredim  23580  trpredss  23636  trpredmintr  23638  dftrpred3g  23640  poseq  23657  wfrlem5  23664  wfrlem13  23672  frrlem5  23689  frrlem5b  23690  frrlem5d  23692  elno2  23711  nofv  23714  noreson  23717  sltres  23721  noxpsgn  23722  axsltsolem1  23725  axdenselem3  23741  axdenselem4  23742  axdenselem6  23744  axdenselem8  23746  axdense  23747  nocvxminlem  23748  axfelem5  23754  axfelem9  23758  axfelem10  23759  axfelem14  23763  axfelem15  23764  axfelem18  23767  axfelem20  23769  axfelem21  23770  axfelem22  23771  brbigcup  23849  funpartfv  23893  altopeq12  23906  axlowdimlem13  23992  axlowdim1  23997  colinearex  24093  btwnconn1lem14  24133  hilbert1.1  24187  hilbert1.2  24188  lineintmo  24190  bpolylem  24193  rankeq1o  24211  elhf2  24215  hfsn  24219  waj-ax  24263  nandsym1  24271  onsucconi  24286  onsucsuccmpi  24292  limsucncmpi  24294  areacirclem2  24335  areacirclem5  24339  areacirclem6  24340  eqintg  24371  imunt  24407  evpexun  24408  elo  24451  neiopne  24461  domfldrefc  24467  ranfldrefc  24468  domrngref  24470  domintrefb  24473  imgfldref2  24474  srefwref  24477  restidsing  24486  imfstnrelc  24491  fixpc  24504  trunitr  24519  uncum2  24520  repfuntw  24571  tolat  24697  vecax3  24866  glmrngo  24893  svli2  24895  svs2  24898  basexre  24933  osneisi  24942  intopcoaconlem3b  24949  intopcoaconb  24951  qusp  24953  istopx  24958  prtoptop  24960  iscnp4  24974  bwt2  25003  altretop  25011  dmse1  25014  iintlem1  25021  trnij  25026  claddrvr  25059  zernpl  25064  cnegvex2  25071  cnegvex2b  25073  rnegvex2b  25074  issubcv  25081  issubrv  25083  dmrngcmp  25162  imonclem  25224  ismonc  25225  iepiclem  25234  isepic  25235  infemb  25270  vtarsu  25297  rocatval  25370  1iskle  25400  lemindclsbu  25406  indcls2  25407  xindcls  25408  empklst  25420  clscnc  25421  cndpv  25460  pgapspf  25463  pgapspf2  25464  aline  25485  isconcl5a  25512  isconcl5ab  25513  isconcl7a  25516  lppotos  25555  bsstrs  25557  nbssntrs  25558  bosser  25578  pdiveql  25579  hpd  25580  abhp  25584  bhp3  25588  finminlem  25642  gtinf  25645  opnrebl2  25647  ntruni  25656  clsint2  25658  isfne  25679  isfne4  25680  isfne4b  25681  fneint  25688  isref  25690  topfneec  25702  fnessref  25704  islocfin  25707  comppfsc  25718  neibastop1  25719  neibastop2lem  25720  neibastop3  25722  topmeet  25724  topjoin  25725  fnemeet1  25726  fnemeet2  25727  fnejoin1  25728  fnejoin2  25729  tailfb  25737  filnetlem3  25740  filnetlem4  25741  cover2  25769  indexa  25823  sdclem2  25863  sdclem1  25864  fdc  25866  seqpo  25868  incsequz2  25870  nnubfi  25871  nninfnub  25872  sstotbnd2  25909  sstotbnd3  25911  equivtotbnd  25913  isbnd3  25919  ssbnd  25923  totbndbnd  25924  prdsbnd  25928  prdstotbnd  25929  cntotbnd  25931  ismtyhmeolem  25939  heibor1lem  25944  heibor1  25945  heiborlem1  25946  heiborlem3  25948  heiborlem7  25952  heiborlem8  25953  heibor  25956  rrnequiv  25970  isdrngo2  26000  0idl  26061  divrngidl  26064  intidl  26065  unichnidl  26067  keridl  26068  ispridl2  26074  maxidln0  26081  igenval  26097  igenidl  26099  igenval2  26102  prnc  26103  isfldidl  26104  ispridlc  26106  prtlem90  26134  eqrelrdvOLD  26139  erprt  26152  elrfi  26180  ismrcd1  26184  ismrcd2  26185  istopclsd  26186  isnacs3  26196  constmap  26199  mapfzcons  26204  ofmpteq  26208  mzpclall  26216  mzpincl  26223  mzpexpmpt  26234  mzpindd  26235  mzpcompact2lem  26240  coeq0i  26243  eldiophb  26247  diophrw  26249  eldioph2lem1  26250  eldioph2lem2  26251  eldioph2b  26253  rabdiophlem1  26293  rabdiophlem2  26294  rexzrexnn0  26296  eldioph4i  26306  fphpd  26310  fiphp3d  26313  rencldnfi  26315  pellexlem4  26328  pellexlem6  26330  pellqrex  26375  pellfundre  26377  pellfundge  26378  pellfundglb  26381  rmxyelqirr  26406  jm2.23  26500  setindtr  26528  dford3lem2  26531  dford3  26532  wopprc  26534  wdom2d2  26539  ttac  26540  fnwe2lem1  26558  fnwe2lem2  26559  fnwe2lem3  26560  fnwe2  26561  aomclem5  26566  dfac11  26571  kelac1  26572  kelac2  26574  dfac21  26575  filnm  26603  dsmmfi  26615  dsmm0cl  26617  frlmgsum  26643  uvcresum  26653  frlmlbs  26660  unxpwdom3  26667  dfacbasgrp  26684  hbtlem2  26739  hbtlem5  26743  hbtlem6  26744  hbt  26745  aaitgo  26778  itgoss  26779  rgspnval  26784  rgspncl  26785  rngunsnply  26789  f1omvdco3  26803  symggen2  26823  psgnunilem5  26828  psgnghm  26848  psgnghm2  26849  matbas2  26886  mendrng  26911  sdrgacs  26920  idomsubgmo  26925  hashgcdeq  26928  phisum  26929  pm13.194  27023  trelpss  27071  rfcnpre1  27101  rspcegf  27105  sumsnd  27108  cnfex  27110  fnchoice  27111  refsumcn  27112  rfcnpre2  27113  cncmpmax  27114  rfcnnnub  27118  fmul01lt1lem1  27125  fmul01lt1lem2  27126  climsuse  27145  dvcosre  27152  itgsinexplem1  27159  stoweidlem3  27163  stoweidlem7  27167  stoweidlem11  27171  stoweidlem14  27174  stoweidlem16  27176  stoweidlem17  27177  stoweidlem23  27183  stoweidlem25  27185  stoweidlem26  27186  stoweidlem27  27187  stoweidlem28  27188  stoweidlem31  27191  stoweidlem34  27194  stoweidlem35  27195  stoweidlem36  27196  stoweidlem39  27199  stoweidlem42  27202  stoweidlem44  27204  stoweidlem46  27206  stoweidlem47  27207  stoweidlem49  27209  stoweidlem51  27211  stoweidlem52  27212  stoweidlem54  27214  stoweidlem57  27217  stoweidlem59  27219  stoweidlem60  27220  wallispilem3  27227  wallispilem4  27228  wallispi  27230  wallispi2lem1  27231  stirlinglem5  27238  stirlinglem8  27241  2rexreu  27354  2reu4a  27358  funresfunco  27379  funcoressn  27381  afvpcfv0  27400  afvfvn0fveq  27404  afvelrn  27421  vk15.4j  27574  tratrb  27582  truniALT  27588  hbexg  27605  2uasbanh  27610  uunT1  27835  sspwtrALT2  27877  pwtrOLD  27879  pwtrrOLD  27881  snssiALT  27883  suctrALT2  27893  en3lpVD  27901  trintALT  27937  bnj145  28034  bnj168  28037  bnj219  28040  bnj534  28047  bnj596  28054  bnj927  28079  bnj1142  28100  bnj1143  28101  bnj1185  28105  bnj1198  28107  bnj1209  28108  bnj1361  28140  bnj1366  28141  bnj1379  28142  bnj1476  28158  bnj1542  28168  bnj110  28169  bnj97  28177  bnj149  28186  bnj150  28187  bnj535  28201  bnj545  28206  bnj546  28207  bnj548  28208  bnj553  28209  bnj571  28217  bnj605  28218  bnj594  28223  bnj580  28224  bnj607  28227  bnj600  28230  bnj917  28245  bnj934  28246  bnj944  28249  bnj964  28254  bnj966  28255  bnj967  28256  bnj969  28257  bnj910  28259  bnj978  28260  bnj986  28265  bnj996  28266  bnj1006  28270  bnj1090  28288  bnj1097  28290  bnj1110  28291  bnj1118  28293  bnj1121  28294  bnj1128  28299  bnj1137  28304  bnj1176  28314  bnj1177  28315  bnj1186  28316  bnj1189  28318  bnj1228  28320  bnj1204  28321  bnj1253  28326  bnj1296  28330  bnj1384  28341  bnj1388  28342  bnj1398  28343  bnj1408  28345  bnj1417  28350  bnj1421  28351  bnj1463  28364  bnj1312  28367  bnj1498  28370  bnj60  28371  a12study  28411  ax9lem12  28430  ax9lem15  28433  lsatlspsn2  28461  lpssat  28482  lssat  28485  lkreqN  28639  glbconN  28845  atex  28874  2llnmat  28992  4atlem3a  29065  dalem18  29149  pmap1N  29235  2lnat  29252  dalawlem10  29348  pclunN  29366  pclfinN  29368  pol1N  29378  osumcllem10N  29433  osumcllem11N  29434  pexmidlem7N  29444  pexmidlem8N  29445  lhpocnel2  29487  4atex2-0bOLDN  29547  cdleme0nex  29758  cdlemg31b0N  30162  cdlemg31b0a  30163  cdlemh  30285  cdlemk36  30381  cdlemk19w  30440  diaval  30501  dia1N  30522  docaclN  30593  dibglbN  30635  diblss  30639  dicval  30645  dihvalrel  30748  dihwN  30758  dihglblem2aN  30762  dihglblem4  30766  dihglbcpreN  30769  dih1dimatlem  30798  dihatlat  30803  dihglblem6  30809  dihjat1  30898  dvh2dim  30914  lpolconN  30956  lcfl8b  30973  lcfrlem4  31014  lcfrlem5  31015  lcfrlem6  31016  lcfrlem16  31027  lcfrlem27  31038  lcfrlem37  31048  lcfr  31054  mapdordlem2  31106  mapdpglem3  31144  mapdhcl  31196  mapdh6dN  31208  mapdh8  31258  hdmap1l6d  31283  hdmap10  31312  hdmaprnlem17N  31335  hdmap14lem14  31353  hdmaplkr  31385  hdmapip0  31387  hgmapvv  31398
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator