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

Theorem sylibr 205
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 199 . 2  |-  ( ps 
->  ch )
41, 3syl 17 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  pm5.74rd  241  bitri  242  3imtr4i  259  con2bid  321  sylanbrc  648  oplem1  935  3mix1  1129  3mix2  1130  3jca  1137  syl3anbrc  1141  inegd  1329  cad11  1395  had1  1398  nfxfrd  1563  19.29r  1596  ax12o10lem4  1638  ax12o10lem8  1642  ax12olem18  1652  ax12olem22  1656  nfd  1707  19.8a  1758  19.39  1792  19.24  1793  19.34  1798  nfim1  1805  nfan1  1806  a4ime  1869  sbn  1955  a4sbe  1968  nfdv  2016  ax11eq  2109  ax11el  2110  mo  2140  eu2  2143  exmo  2163  2exeu  2195  2mo  2196  2eu6  2203  bm1.1  2243  eqrdv  2256  3eltr4g  2341  abbi2dv  2373  abbi1dv  2374  nfcd  2389  nfcxfrd  2392  3netr4g  2450  necon3ai  2461  alral  2576  ra4e  2579  ra42e  2581  rgen2a  2584  ralrimi  2599  r19.27av  2656  mormo  2727  nrexrmo  2732  cgsex2g  2795  cgsex4g  2796  cla42egv  2845  cla43egv  2847  rcla4e  2854  ceqex  2873  mo2icl  2919  reu3  2930  reu6i  2931  sbc5  2990  ra4esbca  3046  rmo2i  3052  sbnfc2  3116  ssrdv  3160  3sstr4g  3194  syl5eqss  3197  ss2abdv  3221  abssdv  3222  rabssdv  3228  ss2rabdv  3229  ssun1  3313  unssad  3327  unssbd  3328  uneqin  3395  reuss2  3423  ne0i  3436  reximdva0  3441  minel  3485  uneqdifeq  3517  disjsn2  3668  absneu  3675  rabsneu  3676  elunii  3806  dfnfc2  3819  uniss2  3832  unidif  3833  ssunieq  3834  intab  3866  iunss2  3921  iunxdif2  3924  riinrab  3951  invdisj  3986  disjiun  3987  disjxiun  3994  3brtr4g  4029  trin  4097  triun  4100  truni  4101  trint  4102  iinexg  4147  class2seteq  4151  notzfaus  4157  pwuni  4178  snelpwi  4192  copsex2t  4225  euotd  4239  opthwiener  4240  ispod  4294  sotric  4312  isso2i  4318  somo  4320  exse  4329  frc  4331  fr2nr  4343  epfrc  4351  trssord  4381  ordelord  4386  ordtri1  4397  orddisj  4402  suctr  4447  trsuc2OLD  4449  eusvnf  4501  eusvnfb  4502  eusv2nf  4504  reusv6OLD  4517  ralxfr2d  4522  rabxfrd  4527  reuhypd  4533  eldifpw  4538  elpwun  4539  elpwunsn  4540  iunpw  4542  fr3nr  4543  ordon  4546  ssorduni  4549  ssonprc  4555  onint0  4559  onminex  4570  suceloni  4576  ordsucss  4581  ordsucelsuc  4585  ordsucuniel  4587  nlimsucg  4605  ordunisuc2  4607  ordzsl  4608  tfi  4616  peano5  4651  eqrelrdv  4771  xpsspw  4785  xpsspwOLD  4786  relint  4797  relop  4822  opeldm  4870  elres  4978  relssres  4980  exse2  5035  issref  5044  trin2  5054  dminss  5083  imainss  5084  xpnz  5087  soex  5110  dmmptg  5157  relrelss  5183  cnviin  5199  funmo  5210  funco  5230  funun  5234  funprg  5239  funtp  5241  fununi  5254  funcnvuni  5255  funimaexg  5267  isarep2  5270  fnunsn  5289  2elresin  5293  fnimadisj  5302  fco  5336  funssxp  5340  fssres  5346  feu  5355  fimacnvdisj  5357  fabexg  5360  f00  5364  f1co  5384  fores  5398  foco  5399  foconst  5400  f1ores  5425  foimacnv  5428  f1oun  5430  fun11iun  5431  f1oco  5434  fo00  5447  fv3  5474  tz6.12-1  5477  nfunsn  5492  dffv2  5526  funfvbrb  5572  respreima  5588  iinpreima  5589  fvelrn  5595  dff2  5606  dff3  5607  dffo4  5610  exfo  5612  ffvresb  5624  fsn  5630  fpr  5638  fsnunf  5652  fsnunfv  5654  zfrep6  5682  elabrex  5699  dff1o6  5725  foeqcnvco  5738  fveqf1o  5740  fliftel1  5743  soisoi  5759  isocnv3  5763  isores1  5765  isoini2  5770  wemoiso  5789  wemoiso2  5790  knatar  5791  eloprabga  5868  fnoprabg  5879  oprabexd  5894  ndmovass  5942  ndmovdistr  5943  fo1stres  6077  fo2ndres  6078  unielxp  6092  1st2ndbr  6103  fmpt2co  6136  1stconst  6141  2ndconst  6142  curry1  6144  cnvf1olem  6150  frxp  6159  poxp  6161  soxp  6162  fnse  6166  reldmtpos  6176  tposfun  6184  dftpos4  6187  sorpssi  6217  sorpssuni  6220  sorpssint  6221  sorpsscmpl  6222  sniota  6252  pwuninel  6268  undefnel  6271  riotasbc  6288  onfununi  6326  onnseq  6329  smores  6337  smores2  6339  smogt  6352  tfrlem9a  6370  tfrlem10  6371  tfr3  6383  tz7.48lem  6421  tz7.48-1  6423  tz7.49  6425  tz7.49c  6426  seqomlem2  6431  seqomlem4  6433  abianfp  6439  2oconcl  6470  oawordeulem  6520  oalimcl  6526  oacomf1o  6531  omlimcl  6544  omeulem1  6548  oeordi  6553  oelim2  6561  oeeulem  6567  oaabslem  6609  oaabs2  6611  omabslem  6612  omabs  6613  brdifun  6655  swoso  6659  ecelqsdm  6697  iiner  6699  qsdisj2  6705  eroveu  6721  erovlem  6722  ecopovtrn  6729  th3qlem1  6732  pmsspw  6770  map0b  6774  mapsn  6777  mapsncnv  6782  ixpf  6806  uniixp  6807  ixpexg  6808  resixp  6819  relsdom  6838  f1oen3g  6845  ssdomg  6875  domtr  6882  domdifsn  6913  omxpenlem  6931  omf1o  6933  sbthlem2  6940  sbthlem3  6941  sbthlem7  6945  sbthlem8  6946  sdomdif  6977  2pwuninel  6984  2pwne  6985  domss2  6988  xpf1o  6991  xpmapenlem  6996  mapdom2  7000  limenpsi  7004  infensuc  7007  php3  7015  1sdom  7033  ominf  7043  isinf  7044  fineqvlem  7045  pssnn  7049  ssnnfi  7050  ssfi  7051  xpfir  7053  dif1enOLD  7058  dif1en  7059  findcard  7065  findcard2  7066  findcard3  7068  ac6sfi  7069  frfi  7070  unblem1  7077  unblem2  7078  nnsdomg  7084  unfi  7092  domunfican  7097  fodomfi  7103  unifi2  7114  pwfilem  7118  pwfi  7119  fissuni  7128  fipreima  7129  finsschain  7130  indexfi  7131  fival  7134  fiin  7143  dffi2  7144  fisn  7148  dffi3  7152  marypha1lem  7154  supmo  7171  suppr  7187  ordtypelem2  7202  ordtypelem3  7203  ordtypelem9  7209  hartogslem1  7225  wemapso2lem  7233  wemapso2  7235  card2inf  7237  wdom2d  7262  wdomd  7263  xpwdomg  7267  ixpiunwdom  7273  inf3lem3  7299  inf3lem6  7302  infdifsn  7325  cantnfle  7340  cantnflt  7341  cantnff  7343  cantnfp1lem2  7349  cantnfp1lem3  7350  oemapvali  7354  cantnflem1a  7355  cantnflem1b  7356  cantnflem1c  7357  cantnflem1  7359  cantnf  7363  wemapwe  7368  oef1o  7369  cnfcom2lem  7372  cnfcom2  7373  cnfcom3lem  7374  cnfcom3  7375  trcl  7378  setind  7387  tcmin  7394  r1ordg  7418  r1pwss  7424  r1val1  7426  tz9.12lem1  7427  tz9.12lem3  7429  tz9.13  7431  r1elwf  7436  rankdmr1  7441  pwwf  7447  unwf  7450  uniwf  7459  rankr1c  7461  rankpwi  7463  rankval3b  7466  rankonidlem  7468  r1pw  7485  r1pwOLD  7486  r1pwcl  7487  rankuni2b  7493  rankelun  7512  rankelpr  7513  rankelop  7514  rankxplim3  7519  rankxpsuc  7520  tcwf  7521  tcrank  7522  scottex  7523  scott0  7524  hta  7535  cardf2  7544  isnumi  7547  tskwe  7551  cardid2  7554  carden2b  7568  cardsn  7570  cardprclem  7580  harval2  7598  dif1card  7606  r0weon  7608  infxpenlem  7609  infxpenc  7613  fseqdom  7621  dfac8clem  7627  ac5num  7631  ondomen  7632  acni2  7641  finacn  7645  acndom2  7649  infpwfien  7657  alephnbtwn  7666  alephsucdom  7674  infenaleph  7686  dfac5lem4  7721  dfac5  7723  dfac2a  7724  dfac2  7725  dfac9  7730  dfacacn  7735  dfac13  7736  dfac12lem2  7738  kmlem4  7747  kmlem6  7749  kmlem8  7751  kmlem13  7756  cda1en  7769  cdainflem  7785  pwsdompw  7798  infdif  7803  infmap2  7812  ackbij1lem18  7831  cff  7842  cflm  7844  cardcf  7846  cfsuc  7851  cff1  7852  cfflb  7853  cflim3  7856  cflim2  7857  cfss  7859  cfslb  7860  cofsmo  7863  cfsmolem  7864  coftr  7867  isfin3  7890  fin23lem7  7910  enfin2i  7915  fin23lem26  7919  fin23lem30  7936  fin23lem32  7938  fin23lem38  7943  fin23lem40  7945  fin23lem41  7946  isf32lem2  7948  isf32lem3  7949  compsscnvlem  7964  compssiso  7968  isf34lem5  7972  isf34lem7  7973  isf34lem6  7974  isfin1-2  7979  isfin1-3  7980  fin56  7987  fin1a2lem11  8004  fin1a2lem13  8006  fin1a2s  8008  hsmexlem2  8021  domtriomlem  8036  dcomex  8041  axdc2lem  8042  axdc3lem  8044  axdc3lem2  8045  axdc3lem4  8047  axdc4lem  8049  axcclem  8051  ac6c4  8076  ac9  8078  ac9s  8088  zorn2lem6  8096  zorn2lem7  8097  zorng  8099  ttukeylem1  8104  ttukeylem6  8109  ttukeylem7  8110  axdclem  8114  brdom3  8121  brdom5  8122  brdom4  8123  iunfo  8129  iundom2g  8130  entric  8147  entri2  8148  ondomon  8153  ficard  8155  konigthlem  8158  alephval2  8162  pwcfsdom  8173  fpwwe2lem1  8221  fpwwe2lem12  8231  fpwwe2lem13  8232  fpwwe2  8233  fpwwe  8236  canthnumlem  8238  canthwelem  8240  canthwe  8241  canthp1lem2  8243  pwfseqlem1  8248  pwfseqlem3  8250  pwfseqlem4a  8251  pwfseqlem4  8252  pwfseqlem5  8253  gchac  8263  hargch  8267  alephgch  8268  gch2  8269  gch3  8270  wunfi  8311  intwun  8325  wunex2  8328  wuncval  8332  wunccl  8334  wuncval2  8337  tsksuc  8352  tskwe2  8363  inttsk  8364  inar1  8365  tskuni  8373  ingru  8405  gruina  8408  grur1a  8409  grur1  8410  axgroth3  8421  inaprc  8426  tskmcl  8431  nqerf  8522  recmulnq  8556  dmrecnq  8560  genpn0  8595  genpnnp  8597  genpcl  8600  nqpr  8606  psslinpr  8623  prlem934  8625  ltexprlem1  8628  ltexprlem4  8631  ltexprlem5  8632  ltexprlem7  8634  reclem2pr  8640  reclem3pr  8641  suplem1pr  8644  supexpr  8646  supsrlem  8701  supsr  8702  axaddrcl  8742  axmulrcl  8744  axrnegex  8752  axcnre  8754  axpre-lttrn  8756  wuncn  8760  cnegex  8961  recextlem2  9367  mulnzcnopr  9382  rereccl  9446  lbreu  9672  supmul1  9687  supmullem2  9689  supmul  9690  infmsup  9700  infmrgelb  9702  infmrlb  9703  nnm1nn0  9973  elnnnn0c  9977  nnnegz  9995  elnnz1  10017  zaddcl  10027  uzind  10071  eluz2b2  10258  zsupss  10275  uzwo3  10279  zmin  10280  znq  10288  qaddcl  10300  qmulcl  10302  qreccl  10304  irradd  10308  irrmul  10309  rpnnen1lem1  10310  rpnnen1lem2  10311  rpnnen1lem3  10312  rpnnen1lem5  10314  cnref1o  10317  qbtwnxr  10494  xrinfmss2  10596  elioo4g  10678  difreicc  10734  fzosplit  10866  elfzo0  10871  1mod  10963  fzennn  10997  fseqsupcl  11006  seqf2  11032  seqf1olem1  11052  seqid3  11057  seqz  11061  ser0f  11066  seqof  11070  expcl2lem  11082  1exp  11098  hashkf  11306  hashsng  11323  hashmap  11353  hashbclem  11356  hashbc  11357  hashf1lem1  11359  hashf1lem2  11360  iswrdi  11383  s1cl  11407  cats1un  11442  shftfval  11531  rennim  11690  cnpart  11691  sqrmo  11703  sqrneglem  11718  rexanuz  11795  sqreulem  11809  eqsqrd  11817  limsupgord  11912  limsupval2  11920  limsupgre  11921  rlimi  11953  climeu  11995  lo1res  11999  rlimmptrcl  12047  o1of2  12052  o1rlimmul  12058  lo1mptrcl  12061  o1mptrcl  12062  isercolllem3  12106  isercoll2  12108  caucvgrlem  12111  summolem3  12153  summo  12156  fsumss  12164  fsumsplit  12178  sumsn  12179  sumsplit  12197  fsum2dlem  12199  fsumcom2  12203  fsum0diag2  12211  fsum00  12222  fsumabs  12225  fsumrlim  12235  fsumo1  12236  o1fsum  12237  fsumiun  12245  fsumiunOLD  12247  hashiunOLD  12248  isumsup2  12268  isumltss  12270  infcvgaux2i  12279  mertenslem1  12303  mertenslem2  12304  ef0lem  12323  efcvgfsum  12330  tanval  12371  rpnnen2lem11  12466  rpnnen2  12467  ruclem6  12476  dvdslelem  12536  dvdsfac  12546  divalglem8  12562  bitsfzolem  12588  bitsinv1  12596  bitsinvp1  12603  sadfval  12606  sadcf  12607  smufval  12631  smupf  12632  smuval2  12636  smupvallem  12637  smu01lem  12639  smumullem  12646  gcdcllem3  12655  gcdaddmlem  12670  bezoutlem2  12681  algrf  12706  algcvgblem  12710  isprm2  12729  isprm3  12730  qredeu  12749  isprm5  12754  phicl2  12799  phibndlem  12801  phibnd  12802  dfphi2  12805  hashdvds  12806  phiprmpw  12807  phimullem  12810  odzcllem  12820  odzdvds  12823  pcdvdsb  12884  infpn2  12923  prmreclem1  12926  prmreclem2  12927  prmreclem3  12928  prmreclem4  12929  prmreclem5  12930  prmreclem6  12931  1arith  12937  4sqlem3  12960  4sqlem11  12965  4sqlem19  12973  vdwapf  12982  vdwlem6  12996  vdwlem8  12998  vdwlem9  12999  vdwlem13  13003  vdwnn  13008  ramtlecl  13010  0ram  13030  ram0  13032  ramub1lem1  13036  ramub1lem2  13037  ramub1  13038  setscom  13139  setsid  13150  restsspw  13299  prdshom  13329  imasaddfnlem  13393  imasaddvallem  13394  imasaddflem  13395  imasvscafn  13402  imasvscaf  13404  xpscfn  13424  xpsc0  13425  xpsc1  13426  mremre  13469  mrcuni  13486  submrc  13493  mreexexlem2d  13510  mreexexlem3d  13511  mreexexd  13513  isacs2  13518  isacs1i  13522  mreacs  13523  acsfn  13524  catideu  13540  isssc  13660  isfuncd  13702  funcoppc  13712  idfucl  13718  cofucl  13725  funcres2b  13734  wunfunc  13736  fthoppc  13760  idffth  13770  ressffth  13775  natixp  13789  nati  13792  fuccocl  13801  fucidcl  13802  invfuc  13811  homaf  13825  coapm  13866  setcepi  13883  catciso  13902  evlfcl  13959  curf2cl  13968  uncfcurf  13976  yonedalem4c  14014  yonedalem3b  14016  yonedalem3  14017  yonedainv  14018  drsdirfi  14035  isdrs2  14036  isposd  14052  lubprop  14077  glbprop  14082  isglbd  14184  odupos  14202  poslubmo  14213  ipoval  14220  ipolerval  14222  isacs4lem  14234  isacs5lem  14235  isacs4  14239  isacs3  14240  acsfiindd  14243  acsmapd  14244  mrelatglb  14250  mrelatlub  14252  spwmo  14298  spweu  14299  mhmeql  14404  gsumvallem1  14411  gsumws1  14425  gsumwspan  14431  grpinveu  14479  prdsinvlem  14566  subgint  14604  0subg  14605  cycsubg  14608  subgacs  14615  nsgacs  14616  0nsg  14625  eqgfval  14628  ghmeql  14668  gimco  14695  brgici  14697  gass  14718  symgval  14734  cayley  14752  oppgsubm  14798  oppgsubg  14799  odcl  14814  dfod2  14840  odf1o2  14847  gexcl  14854  gex1  14865  pgpfi1  14869  sylow1lem2  14873  sylow1lem3  14874  odcau  14878  pgpssslw  14888  sylow2alem2  14892  sylow2a  14893  sylow2blem1  14894  sylow2blem3  14896  sylow3lem3  14903  sylow3lem6  14906  pj1fval  14966  efgrcl  14987  efgval  14989  efgi  14991  efgi2  14997  efgsval2  15005  efgs1  15007  efgs1b  15008  efgsp1  15009  efgsres  15010  efgsfo  15011  efgredlemd  15016  efgredlem  15019  efgrelexlemb  15022  0frgp  15051  iscmnd  15064  gexex  15108  frgpnabllem1  15124  iscygodd  15138  prmcyg  15143  lt6abl  15144  gsumval3eu  15153  gsumval3  15154  gsumzaddlem  15166  gsumzsplit  15169  gsummhm2  15175  gsumunsn  15184  gsumpt  15185  gsum2d  15186  gsumcom2  15189  eldprd  15202  dprdfadd  15218  dprdspan  15225  dprdres  15226  dprdcntz2  15236  dprd2dlem2  15238  dprd2dlem1  15239  dprd2da  15240  dprd2d2  15242  dmdprdsplit2lem  15243  dpjfval  15253  ablfacrplem  15263  ablfacrp  15264  ablfacrp2  15265  ablfac1b  15268  ablfac1eulem  15270  ablfac1eu  15271  pgpfac1lem5  15277  pgpfaclem1  15279  ablfaclem2  15284  ablfaclem3  15285  ablfac2  15287  pws1  15362  opprrngb  15377  irredn0  15448  isdrngd  15500  isdrngrd  15501  opprsubrg  15529  subrgint  15530  subrgmre  15532  issubdrg  15533  issrngd  15589  lsssn0  15668  lss1d  15683  lssintcl  15684  lssmre  15686  lspf  15694  lspval  15695  lspextmo  15776  brlmici  15785  lsppratlem1  15863  lsppratlem6  15868  lbsextlem1  15874  lbsextlem2  15875  lbsextlem3  15876  lbsextlem4  15877  sraval  15892  rsp1  15939  drngnidl  15944  abvn0b  16006  fidomndrng  16011  aspval  16031  asplss  16032  aspid  16033  aspsubrg  16034  psrbagconcl  16082  psrbagconf1o  16083  psrass1lem  16086  psraddcl  16091  psrmulcllem  16095  psrvscacl  16101  psr0cl  16102  psrnegcl  16104  psr1cl  16110  subrgpsr  16126  mvrf  16132  mplmon  16170  mplcoe1  16172  mplcoe2  16174  opsrtoslem2  16189  subrgasclcl  16203  coe1fval3  16252  coe1z  16303  coe1mul2  16309  coe1tm  16312  prmirredlem  16409  mulgrhm2  16424  zlmlmod  16440  zlmassa  16441  znf1o  16468  znfi  16476  znidomb  16478  ipcl  16500  cssmre  16556  obselocv  16591  eltopspOLD  16619  istopon  16626  toponcom  16631  topgele  16635  topontopn  16643  tsettps  16644  tgval  16656  eltg2b  16660  en2top  16686  tgss2  16688  bastop2  16695  distop  16696  fctop  16704  cctop  16706  ppttop  16707  pptbas  16708  epttop  16709  cldss2  16730  clscld  16747  elcls  16773  mretopd  16792  toponmre  16793  neisspw  16807  neips  16813  neiuni  16822  clslp  16842  restbas  16852  resstps  16880  ordtbaslem  16881  ordtbas2  16884  ordtbas  16885  ordttopon  16886  ordtopn1  16887  ordtopn2  16888  ordtrest2  16897  iocpnfordt  16908  icomnfordt  16909  lecldbas  16912  tgcn  16945  tgcnp  16946  subbascn  16947  cnntr  16967  lmff  16992  t0dist  17016  pnrmopn  17034  lpcls  17055  t1sep  17061  dishaus  17073  ordthauslem  17074  cmpcovf  17081  discmp  17088  cmpsublem  17089  cmpsub  17090  fiuncmp  17094  hauscmplem  17096  cmpfi  17098  cnconn  17111  consubclo  17113  iuncon  17117  clscon  17119  concompid  17120  1stcfb  17134  2ndci  17137  2ndcsb  17138  2ndc1stc  17140  1stcrest  17142  2ndcctbss  17144  2ndcdisj  17145  2ndcomap  17147  2ndcsep  17148  dis2ndc  17149  nlly2i  17165  llynlly  17166  restnlly  17171  llyrest  17174  llyidm  17177  nllyidm  17178  hausllycmp  17183  cldllycmp  17184  lly1stc  17185  dislly  17186  llycmpkgen2  17208  1stckgenlem  17211  kgencn2  17215  txuni2  17223  txbasex  17224  txbas  17225  elptr  17231  elptr2  17232  ptbasin2  17236  ptbasfi  17239  xkoopn  17247  xkouni  17257  ptpjopn  17269  ptclsg  17272  dfac14  17275  xkoccn  17276  txcnp  17277  ptcnplem  17278  ptcnp  17279  txcnmpt  17281  txcn  17283  ptcn  17284  prdstopn  17285  txdis  17289  txindis  17291  txdis1cn  17292  txlly  17293  txnlly  17294  pthaus  17295  ptrescn  17296  txtube  17297  txcmplem1  17298  txcmplem2  17299  tx1stc  17307  xkohaus  17310  xkococnlem  17316  xkococn  17317  cnmpt11  17320  cnmpt1t  17322  cnmpt12  17324  cnmpt21  17328  cnmpt2t  17330  cnmpt22  17331  cnmptkp  17337  cnmptk1  17338  cnmpt1k  17339  cnmptkk  17340  cnmptk1p  17342  cnmptk2  17343  cnmpt2k  17345  txcon  17346  qtoptop2  17353  qtopuni  17356  basqtop  17365  tgqtop  17366  qtopeu  17370  imastps  17375  kqdisj  17386  kqcldsat  17387  kqt0  17400  kqreg  17405  kqnrm  17406  hmeofval  17412  hmphi  17431  hmphdis  17450  ordthmeolem  17455  xpstopnlem1  17463  ptcmpfi  17467  reghaus  17479  fbssfi  17495  fbssint  17496  opnfbas  17500  trfbas2  17501  isfil2  17514  snfil  17522  fsubbas  17525  fgcl  17536  neifil  17538  fbasrn  17542  filuni  17543  supfil  17553  uzrest  17555  uzfbas  17556  isufil2  17566  filssufilg  17569  numufl  17573  fixufil  17580  uffixsn  17583  rnelfmlem  17610  hausflimi  17638  flimsncls  17644  hauspwpwf1  17645  flftg  17654  txflf  17664  fclscmp  17688  alexsublem  17701  alexsub  17702  alexsubb  17703  alexsubALTlem2  17705  alexsubALTlem3  17706  alexsubALTlem4  17707  ptcmplem3  17711  ptcmplem4  17712  cnmpt1plusg  17733  cnmpt2plusg  17734  tmdgsum  17741  oppgtmd  17743  distgp  17745  indistgp  17746  symgtgp  17747  clssubg  17754  clsnsg  17755  cldsubg  17756  tgpconcompeqg  17757  tgpconcomp  17758  ghmcnp  17760  divstgplem  17766  tsmsfbas  17773  tsmsid  17785  tsmsf1o  17790  tgptsmscls  17795  tsmssplit  17797  tsmsxp  17800  cnmpt1vsca  17839  cnmpt2vsca  17840  prdsxmetlem  17895  imasdsf1olem  17900  blbas  17939  setsmstopn  17987  prdsbl  18000  blsscls2  18013  met1stc  18030  met2ndci  18031  prdsxmslem2  18038  tngtopn  18129  nrgtrg  18163  tgqioo  18269  zdis  18285  iccntr  18289  icccmplem1  18290  icccmplem2  18291  reconnlem1  18294  cnmpt1ds  18310  cnmpt2ds  18311  metdsf  18315  metnrmlem3  18328  fsumcn  18337  cncfmpt1f  18380  cncfmpt2ss  18382  cnmpt2pc  18389  icoopnst  18400  iocopnst  18401  cnllycmp  18417  evth  18420  lebnumlem1  18422  copco  18479  pcoass  18485  pi1xfrcnv  18518  zlmclm  18556  cnmpt1ip  18637  cnmpt2ip  18638  cfilres  18685  bcthlem5  18713  bcth  18714  minveclem1  18751  minveclem2  18753  minveclem3b  18755  minveclem4a  18757  pmltpc  18773  evthicc2  18783  ovolficcss  18792  ovolfsf  18794  ovolsf  18795  elovolmr  18798  ovolgelb  18802  ovolunlem1  18819  ovolfiniun  18823  ovoliunlem1  18824  ovoliunlem2  18825  ovoliun  18827  ovoliun2  18828  ovoliunnul  18829  ovolshftlem2  18832  ovolicc2lem4  18842  ovolicc2  18844  volfiniun  18867  iundisj  18868  voliunlem1  18870  voliunlem2  18871  voliunlem3  18872  volsup  18876  ovolioo  18888  ioorf  18891  uniioombllem3a  18902  uniioombllem3  18903  uniioombllem6  18906  dyadmax  18916  dyadmbllem  18917  dyadmbl  18918  opnmbllem  18919  volsup2  18923  vitalilem2  18927  vitalilem3  18928  vitalilem4  18929  vitalilem5  18930  vitali  18931  mbfconstlem  18947  mbfmptcl  18955  mbfeqalem  18960  mbfposr  18970  ismbf3d  18972  mbfinf  18983  mbflimsup  18984  mbflim  18986  i1fima2  18997  i1fd  18999  itg1val2  19002  i1fadd  19013  i1fmul  19014  itg1addlem4  19017  i1fmulc  19021  i1fposd  19025  itg1climres  19032  itg2lr  19048  itg2seq  19060  itg2mulc  19065  itg2splitlem  19066  itg2split  19067  itg2monolem1  19068  itg2i1fseq  19073  itg2gt0  19078  itg2cn  19081  iblcnlem  19106  itgss3  19132  itgfsum  19144  itgsplitioo  19155  itggt0  19159  limcvallem  19184  cnmptlimc  19203  limcco  19206  limciun  19207  dvfval  19210  perfdvf  19216  dvnfval  19234  dvcmul  19256  dvcobr  19258  dvmptcl  19271  dvmptco  19284  dvmptfsum  19285  dvcnvlem  19286  dveflem  19289  dvef  19290  dvferm1  19295  rolle  19300  c1liplem1  19306  dvlt0  19315  dvle  19317  dvne0  19321  lhop1lem  19323  dvfsumle  19331  dvfsumge  19332  dvfsumabs  19333  dvmptrecl  19334  dvfsumlem2  19337  itgparts  19357  itgsubstlem  19358  itgsubst  19359  evlseu  19363  mpfrcl  19365  evl1sca  19376  mpfind  19391  pf1rcl  19395  pf1ind  19401  deg1n0ima  19438  ply1divmo  19484  fta1blem  19517  ig1pcl  19524  elply2  19541  plyeq0lem  19555  plypf1  19557  coeeulem  19569  coeeq  19572  plycj  19621  plycpn  19632  vieta1lem1  19653  vieta1lem2  19654  plyexmo  19656  elqaalem1  19662  elqaalem3  19664  aannenlem1  19671  aaliou2  19683  taylfval  19701  taylf  19703  dvtaylp  19712  dvntaylp  19713  taylthlem1  19715  taylthlem2  19716  ulmcau  19735  ulmss  19737  ulmdvlem2  19741  mtest  19744  itgulm2  19748  radcnvlt1  19757  dvradcnv  19760  pserdvlem2  19767  abelthlem2  19771  abelthlem3  19772  sincn  19783  coscn  19784  reeff1o  19786  recosf1o  19860  dvlog  19961  efopn  19968  logtayl  19970  cxple2a  20009  cxpcn3  20051  cxpaddlelem  20054  cxpaddle  20055  ang180lem3  20072  logreclem  20079  isosctrlem2  20082  birthdaylem3  20211  xrlimcnp  20226  efrlim  20227  rlimcxp  20231  jensenlem1  20244  jensenlem2  20245  jensen  20246  fsumharmonic  20268  wilthlem2  20270  basellem9  20289  sgmss  20307  sgmnncl  20348  ppinprm  20353  chtprm  20354  chtnprm  20355  ppiltx  20378  mumul  20382  sqff1o  20383  musum  20394  dvdsmulf1o  20397  fsumdvdsmul  20398  fsumvma  20415  perfectlem2  20432  dchrelbas3  20440  dchrfi  20457  dchrptlem1  20466  dchrptlem2  20467  dchrptlem3  20468  dchrsum2  20470  bcmono  20479  bposlem4  20489  lgslem1  20498  lgsfcl2  20504  lgscllem  20505  lgsval2lem  20508  lgsdir2lem5  20529  lgsne0  20535  lgseisenlem2  20552  lgseisenlem3  20553  lgsquadlem2  20557  2sqlem2  20566  mul2sq  20567  2sqlem3  20568  2sqlem7  20572  2sqlem8  20574  2sqlem11  20577  2sqblem  20579  dchrisumlem3  20603  dchrisum0flblem1  20620  dchrisum0flb  20622  dchrisumn0  20633  pntlem3  20721  qrngdiv  20736  ex-br  20762  ex-natded9.26  20795  isgrpo  20824  grpofo  20827  grpoideu  20837  grpoinveu  20850  isgrpda  20925  ablomul  20983  ghgrp  20996  rngoideu  21012  rngmgmbs4  21045  rngomndo  21049  rngo1cl  21057  nmosetn0  21304  nmoolb  21310  nmlno0lem  21332  blocnilem  21343  blocni  21344  lnocni  21345  ubthlem1  21410  minvecolem1  21414  minvecolem2  21415  minvecolem5  21421  htthlem  21458  bcsiALT  21719  hlimadd  21733  shex  21752  hsn0elch  21788  hhsst  21804  hhsscms  21817  occon  21827  pjhthmo  21842  shscli  21857  choc0  21866  choc1  21867  shintcli  21869  spancl  21876  spanss  21888  ococin  21948  chsupsn  21953  pjoc1i  21971  chlejb1i  22016  chabs2  22057  spanuni  22084  spanunsni  22119  h1datomi  22121  cmbr3i  22140  cmbr4i  22141  lecmi  22142  chscllem2  22178  osumcor2i  22184  nonbooli  22191  pjss2i  22220  pjjsi  22240  pjmf1  22256  hmopex  22416  nmoplb  22448  nmfnlb  22465  nmlnop0iALT  22536  nmopun  22555  lnconi  22574  nmcfnlbi  22593  imaelshi  22599  cnlnadjlem3  22610  cnlnadjlem5  22612  cnlnadjeui  22618  cnlnssadj  22621  adjbdln  22624  adjbdlnb  22625  adjeq0  22632  branmfn  22646  hmopidmpji  22693  pjss2coi  22705  pjnormssi  22709  pjssdif2i  22715  pjinvari  22732  pjci  22741  pjcmul2i  22743  strlem1  22791  mdsl1i  22862  mdslmd3i  22873  csmdsymi  22875  mdexchi  22876  chpssati  22904  atomli  22923  chirredi  22935  mdsymlem6  22949  sumdmdii  22956  cmmdi  22957  sumdmdlem2  22960  dmdbr5ati  22963  dmdbr6ati  22964  dmdbr7ati  22965  cdjreui  22973  cdj3i  22982  nvof1o  22998  ballotlemfc0  23013  ballotlemfcc  23014  ballotlemiex  23022  ballotlemi1  23023  ballotlemii  23024  ballotlemsup  23025  ballotlemfrcn0  23050  subfacp1lem3  23086  subfacp1lem5  23088  subfacp1lem6  23089  erdszelem5  23099  erdszelem7  23101  erdszelem11  23105  kur14lem9  23118  pconcon  23135  txpcon  23136  conpcon  23139  cnllyscon  23149  iccllyscon  23154  rellyscon  23155  cvmcov  23167  cvmsss2  23178  cvmliftmo  23188  cvmlift2lem1  23206  cvmlift2lem12  23218  cvmlift2lem13  23219  cvmlift3lem2  23224  umgraex  23248  umgra1  23251  vdgr1d  23267  vdgr1b  23268  vdgr1a  23270  eupares  23272  eupap1  23273  eupath2lem3  23276  eupath2  23277  eupath  23278  vdegp1ai  23281  vdegp1bi  23282  ghomgrpilem2  23366  climuzcnv  23377  circum  23380  lediv2aALT  23386  relexpindlem  23409  rtrclreclem.trans  23416  rtrclreclem.min  23417  dfrtrcl2  23418  dedekind  23454  relin01  23461  fundmpss  23492  dfon2lem4  23512  dfon2lem5  23513  dfon2lem7  23515  dfon2lem9  23517  dfon2  23518  rdgprc  23521  elpredim  23546  trpredss  23602  trpredmintr  23604  dftrpred3g  23606  poseq  23623  wfrlem5  23630  wfrlem13  23638  frrlem5  23655  frrlem5b  23656  frrlem5d  23658  elno2  23677  nofv  23680  noreson  23683  sltres  23687  noxpsgn  23688  axsltsolem1  23691  axdenselem3  23707  axdenselem4  23708  axdenselem6  23710  axdenselem8  23712  axdense  23713  nocvxminlem  23714  axfelem5  23720  axfelem9  23724  axfelem10  23725  axfelem14  23729  axfelem15  23730  axfelem18  23733  axfelem20  23735  axfelem21  23736  axfelem22  23737  brbigcup  23815  funpartfv  23859  altopeq12  23872  axlowdimlem13  23958  axlowdim1  23963  colinearex  24059  btwnconn1lem14  24099  hilbert1.1  24153  hilbert1.2  24154  lineintmo  24156  bpolylem  24159  rankeq1o  24177  elhf2  24181  hfsn  24185  waj-ax  24229  nandsym1  24237  onsucconi  24252  onsucsuccmpi  24258  limsucncmpi  24260  eqintg  24328  imunt  24364  evpexun  24365  elo  24408  neiopne  24418  domfldrefc  24424  ranfldrefc  24425  domrngref  24427  domintrefb  24430  imgfldref2  24431  srefwref  24434  restidsing  24443  imfstnrelc  24448  fixpc  24461  trunitr  24476  uncum2  24477  repfuntw  24528  tolat  24654  vecax3  24823  glmrngo  24850  svli2  24852  svs2  24855  basexre  24890  osneisi  24899  intopcoaconlem3b  24906  intopcoaconb  24908  qusp  24910  istopx  24915  prtoptop  24917  iscnp4  24931  bwt2  24960  altretop  24968  dmse1  24971  iintlem1  24978  trnij  24983  claddrvr  25016  zernpl  25021  cnegvex2  25028  cnegvex2b  25030  rnegvex2b  25031  issubcv  25038  issubrv  25040  dmrngcmp  25119  imonclem  25181  ismonc  25182  iepiclem  25191  isepic  25192  infemb  25227  vtarsu  25254  rocatval  25327  1iskle  25357  lemindclsbu  25363  indcls2  25364  xindcls  25365  empklst  25377  clscnc  25378  cndpv  25417  pgapspf  25420  pgapspf2  25421  aline  25442  isconcl5a  25469  isconcl5ab  25470  isconcl7a  25473  lppotos  25512  bsstrs  25514  nbssntrs  25515  bosser  25535  pdiveql  25536  hpd  25537  abhp  25541  bhp3  25545  finminlem  25599  gtinf  25602  opnrebl2  25604  ntruni  25613  clsint2  25615  isfne  25636  isfne4  25637  isfne4b  25638  fneint  25645  isref  25647  topfneec  25659  fnessref  25661  islocfin  25664  comppfsc  25675  neibastop1  25676  neibastop2lem  25677  neibastop3  25679  topmeet  25681  topjoin  25682  fnemeet1  25683  fnemeet2  25684  fnejoin1  25685  fnejoin2  25686  tailfb  25694  filnetlem3  25697  filnetlem4  25698  cover2  25726  indexa  25780  sdclem2  25820  sdclem1  25821  fdc  25823  seqpo  25825  incsequz2  25827  nnubfi  25828  nninfnub  25829  sstotbnd2  25866  sstotbnd3  25868  equivtotbnd  25870  isbnd3  25876  ssbnd  25880  totbndbnd  25881  prdsbnd  25885  prdstotbnd  25886  cntotbnd  25888  ismtyhmeolem  25896  heibor1lem  25901  heibor1  25902  heiborlem1  25903  heiborlem3  25905  heiborlem7  25909  heiborlem8  25910  heibor  25913  rrnequiv  25927  isdrngo2  25957  0idl  26018  divrngidl  26021  intidl  26022  unichnidl  26024  keridl  26025  ispridl2  26031  maxidln0  26038  igenval  26054  igenidl  26056  igenval2  26059  prnc  26060  isfldidl  26061  ispridlc  26063  prtlem90  26091  eqrelrdvOLD  26096  erprt  26109  elrfi  26137  ismrcd1  26141  ismrcd2  26142  istopclsd  26143  isnacs3  26153  constmap  26156  mapfzcons  26161  ofmpteq  26165  mzpclall  26173  mzpincl  26180  mzpexpmpt  26191  mzpindd  26192  mzpcompact2lem  26197  coeq0i  26200  eldiophb  26204  diophrw  26206  eldioph2lem1  26207  eldioph2lem2  26208  eldioph2b  26210  rabdiophlem1  26250  rabdiophlem2  26251  rexzrexnn0  26253  eldioph4i  26263  fphpd  26267  fiphp3d  26270  rencldnfi  26272  pellexlem4  26285  pellexlem6  26287  pellqrex  26332  pellfundre  26334  pellfundge  26335  pellfundglb  26338  rmxyelqirr  26363  jm2.23  26457  setindtr  26485  dford3lem2  26488  dford3  26489  wopprc  26491  wdom2d2  26496  ttac  26497  fnwe2lem1  26515  fnwe2lem2  26516  fnwe2lem3  26517  fnwe2  26518  aomclem5  26523  dfac11  26528  kelac1  26529  kelac2  26531  dfac21  26532  filnm  26560  dsmmfi  26572  dsmm0cl  26574  frlmgsum  26600  uvcresum  26610  frlmlbs  26617  unxpwdom3  26624  dfacbasgrp  26641  hbtlem2  26696  hbtlem5  26700  hbtlem6  26701  hbt  26702  aaitgo  26735  itgoss  26736  rgspnval  26741  rgspncl  26742  rngunsnply  26746  f1omvdco3  26760  symggen2  26780  psgnunilem5  26785  psgnghm  26805  psgnghm2  26806  matbas2  26843  mendrng  26868  sdrgacs  26877  idomsubgmo  26882  hashgcdeq  26885  phisum  26886  pm13.194  26981  trelpss  27029  rfcnpre1  27059  rcla4egf  27063  sumsnd  27066  cnfex  27068  fnchoice  27069  refsumcn  27070  rfcnpre2  27071  cncmpmax  27072  rfcnnnub  27076  fmul01lt1lem1  27083  fmul01lt1lem2  27084  climsuse  27103  dvcosre  27110  itgsinexplem1  27117  stoweidlem3  27121  stoweidlem7  27125  stoweidlem11  27129  stoweidlem14  27132  stoweidlem16  27134  stoweidlem17  27135  stoweidlem23  27141  stoweidlem25  27143  stoweidlem26  27144  stoweidlem27  27145  stoweidlem28  27146  stoweidlem31  27149  stoweidlem34  27152  stoweidlem35  27153  stoweidlem36  27154  stoweidlem39  27157  stoweidlem42  27160  stoweidlem44  27162  stoweidlem46  27164  stoweidlem47  27165  stoweidlem49  27167  stoweidlem51  27169  stoweidlem52  27170  stoweidlem54  27172  stoweidlem57  27175  stoweidlem59  27177  stoweidlem60  27178  wallispilem3  27185  wallispilem4  27186  wallispi  27188  wallispi2lem1  27189  stirlinglem5  27196  stirlinglem8  27199  2rexreu  27312  2reu4a  27316  vk15.4j  27427  tratrb  27435  truniALT  27441  hbexg  27458  2uasbanh  27463  uunT1  27688  sspwtrALT2  27730  pwtrOLD  27732  pwtrrOLD  27734  snssiALT  27736  suctrALT2  27746  en3lpVD  27754  trintALT  27790  bnj145  27887  bnj168  27890  bnj219  27893  bnj534  27900  bnj596  27907  bnj927  27932  bnj1142  27953  bnj1143  27954  bnj1185  27958  bnj1198  27960  bnj1209  27961  bnj1361  27993  bnj1366  27994  bnj1379  27995  bnj1476  28011  bnj1542  28021  bnj110  28022  bnj97  28030  bnj149  28039  bnj150  28040  bnj535  28054  bnj545  28059  bnj546  28060  bnj548  28061  bnj553  28062  bnj571  28070  bnj605  28071  bnj594  28076  bnj580  28077  bnj607  28080  bnj600  28083  bnj917  28098  bnj934  28099  bnj944  28102  bnj964  28107  bnj966  28108  bnj967  28109  bnj969  28110  bnj910  28112  bnj978  28113  bnj986  28118  bnj996  28119  bnj1006  28123  bnj1090  28141  bnj1097  28143  bnj1110  28144  bnj1118  28146  bnj1121  28147  bnj1128  28152  bnj1137  28157  bnj1176  28167  bnj1177  28168  bnj1186  28169  bnj1189  28171  bnj1228  28173  bnj1204  28174  bnj1253  28179  bnj1296  28183  bnj1384  28194  bnj1388  28195  bnj1398  28196  bnj1408  28198  bnj1417  28203  bnj1421  28204  bnj1463  28217  bnj1312  28220  bnj1498  28223  bnj60  28224  ax12o10lem4K  28286  ax12o10lem4X  28287  ax12o10lem8K  28294  ax12o10lem8X  28295  ax12olem18K  28315  ax12olem18X  28316  ax12olem22K  28324  ax12olem22X  28325  a12study  28382  ax9lem12  28401  ax9lem15  28404  lsatlspsn2  28432  lpssat  28453  lssat  28456  lkreqN  28610  glbconN  28816  atex  28845  2llnmat  28963  4atlem3a  29036  dalem18  29120  pmap1N  29206  2lnat  29223  dalawlem10  29319  pclunN  29337  pclfinN  29339  pol1N  29349  osumcllem10N  29404  osumcllem11N  29405  pexmidlem7N  29415  pexmidlem8N  29416  lhpocnel2  29458  4atex2-0bOLDN  29518  cdleme0nex  29729  cdlemg31b0N  30133  cdlemg31b0a  30134  cdlemh  30256  cdlemk36  30352  cdlemk19w  30411  diaval  30472  dia1N  30493  docaclN  30564  dibglbN  30606  diblss  30610  dicval  30616  dihvalrel  30719  dihwN  30729  dihglblem2aN  30733  dihglblem4  30737  dihglbcpreN  30740  dih1dimatlem  30769  dihatlat  30774  dihglblem6  30780  dihjat1  30869  dvh2dim  30885  lpolconN  30927  lcfl8b  30944  lcfrlem4  30985  lcfrlem5  30986  lcfrlem6  30987  lcfrlem16  30998  lcfrlem27  31009  lcfrlem37  31019  lcfr  31025  mapdordlem2  31077  mapdpglem3  31115  mapdhcl  31167  mapdh6dN  31179  mapdh8  31229  hdmap1l6d  31254  hdmap10  31283  hdmaprnlem17N  31306  hdmap14lem14  31324  hdmaplkr  31356  hdmapip0  31358  hgmapvv  31369
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator