MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6sseqr Structured version   Visualization version   GIF version

Theorem syl6sseqr 3860
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl6ssr.1 (𝜑𝐴𝐵)
syl6ssr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6sseqr (𝜑𝐴𝐶)

Proof of Theorem syl6sseqr
StepHypRef Expression
1 syl6ssr.1 . 2 (𝜑𝐴𝐵)
2 syl6ssr.2 . . 3 𝐶 = 𝐵
32eqcomi 2826 . 2 𝐵 = 𝐶
41, 3syl6sseq 3859 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-in 3787  df-ss 3794
This theorem is referenced by:  disjxiun  4852  knatar  6841  iunpw  7218  wfrdmcl  7669  wfrlem12  7672  wfrlem16  7676  wfrlem17  7677  tfrlem9  7727  tfrlem9a  7728  tfrlem13  7732  tz7.44-2  7749  tz7.44-3  7750  tz7.49  7786  marypha1lem  8588  ordtypelem2  8673  ixpiunwdom  8745  oemapvali  8838  tcss  8877  tcel  8878  pwwf  8927  rankpwi  8943  rankval3b  8946  cplem1  9009  dfac12lem2  9261  infmap2  9335  ackbij1b  9356  ttukeylem6  9631  fpwwe2lem11  9757  fpwwe2lem12  9758  fpwwe2lem13  9759  fpwwe2  9760  uznnssnn  11973  shftfval  14053  rexuzre  14335  climsup  14643  clim2prod  14861  fprodntriv  14913  eulerthlem2  15724  ramtlecl  15941  mreexexlem4d  16532  mreexdomd  16534  gsumpropd2lem  17498  gsumzaddlem  18542  gsum2d  18592  telgsums  18612  pgpfac1lem1  18695  pgpfac1lem3a  18697  pgpfac1lem3  18698  pgpfac1lem5  18700  lspsolvlem  19370  lbsextlem2  19388  dsmmacl  20316  eltopss  20946  difopn  21073  tgrest  21198  perfopn  21224  pnfnei  21259  mnfnei  21260  regsep2  21415  cncmp  21430  uncmp  21441  hauscmplem  21444  hauscmp  21445  conndisj  21454  cnconn  21460  conncompss  21471  2ndcctbss  21493  islly2  21522  comppfsc  21570  1stckgenlem  21591  txuni2  21603  ptbasfi  21619  ptpjopn  21650  txindis  21672  txtube  21678  hausdiag  21683  xkoinjcn  21725  tgqtop  21750  filconn  21921  elfm2  21986  flimclslem  22022  flffbas  22033  fclsbas  22059  flimfnfcls  22066  alexsubALT  22089  symgtgp  22139  ustssco  22252  isucn2  22317  ucnima  22319  ucnprima  22320  blcls  22545  prdsxmslem2  22568  isngp2  22635  tgioo  22833  xrtgioo  22843  xrsmopn  22849  opnreen  22868  cnheiborlem  22987  cnllycmp  22989  tchcph  23269  rrxmvallem  23422  uniioombllem4  23590  dyadmbllem  23603  opnmbllem  23605  mbfimaopnlem  23659  mbflimsup  23670  i1fadd  23699  i1fmul  23700  itg1addlem4  23703  i1fmulc  23707  limciun  23895  dvlip2  23995  c1lip3  23999  lhop  24016  dvfsumlem2  24027  dvfsumrlimge0  24030  dvfsumrlim2  24032  ulmval  24371  psercnlem2  24415  efopnlem2  24640  efopn  24641  umgrres1lem  26441  upgrres1  26444  nbgrssvwo2  26497  nbgrssvwo2OLD  26500  ubthlem1  28077  issh2  28417  mdsymlem1  29613  padct  29847  xrofsup  29883  fz2ssnn0  29897  tpr2rico  30306  sibfinima  30749  fct2relem  31023  bnj906  31345  bnj1014  31375  bnj1286  31432  bnj1408  31449  bnj1450  31463  bnj1452  31465  bnj1498  31474  bnj1501  31480  cvmopnlem  31605  cvmfolem  31606  cvmliftlem6  31617  cvmliftlem8  31619  cvmliftlem13  31623  cvmliftlem15  31625  cvmlift2lem9  31638  cvmlift2lem11  31640  cvmlift2lem12  31641  mclsppslem  31825  trpredpred  32070  trpredtr  32072  trpredrec  32080  frrlem5e  32131  frrlem11  32135  filnetlem4  32719  dissneqlem  33523  lindsdom  33735  opnmbllem0  33777  cnambfre  33789  heibor1lem  33938  osumcllem1N  35755  osumcllem2N  35756  pexmidlem6N  35774  dochexmidlem6  37264  dochexmidlem7  37265  mapdrvallem3  37445  k0004ss2  38968  dvsconst  39047  dvsid  39048  dvsef  39049  iunconnlem2  39683  uzssd2  40141  climinf  40336  climsuse  40338  climresmpt  40389  climleltrp  40406  stoweidlem28  40742  stoweidlem50  40764  stoweidlem52  40766  stoweidlem53  40767  stoweidlem54  40768  fourierdlem54  40874  fourierdlem80  40900  meaiininclem  41200  caratheodorylem2  41241  hspmbllem2  41341  mbfresmf  41448  smfmbfcex  41468  smflimlem2  41480  smflimsuplem2  41527  smflimsuplem3  41528  smflimsuplem5  41530  smflimsuplem6  41531  pfxccatpfx2  42021  upgredgssspr  42337  setrec1  43024  setrecsres  43034  aacllem  43136
  Copyright terms: Public domain W3C validator