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

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

Proof of Theorem syl6sseq
StepHypRef Expression
1 syl6sseq.1 . 2 (𝜑𝐴𝐵)
2 syl6sseq.2 . . 3 𝐵 = 𝐶
32sseq2i 3827 . 2 (𝐴𝐵𝐴𝐶)
41, 3sylib 209 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3769
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 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
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 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  syl6sseqr  3849  sofld  5792  relrelss  5873  foimacnv  6366  onfununi  7670  hartogslem1  8682  cantnfp1lem3  8820  uniwf  8925  rankeq0b  8966  cflecard  9356  fin23lem16  9438  fin23lem41  9455  pwcfsdom  9686  fpwwe2lem13  9745  fpwwe2  9746  canth4  9750  hashbclem  13449  dmtrclfv  13978  zsum  14668  fsumcvg3  14679  incexclem  14786  zprod  14884  ramub1lem1  15943  setsstruct2  16103  imasaddfnlem  16389  imasvscafn  16398  mremre  16465  submre  16466  mreexexlem3d  16507  isacs1i  16518  acsmapd  17379  acsmap2d  17380  gsumzoppg  18541  lspsntri  19300  lsppratlem4  19355  lbsextlem3  19365  distop  21009  elcls  21087  cnpresti  21302  cnprest  21303  cmpcld  21415  cnconn  21435  iunconn  21441  comppfsc  21545  ptuni2  21589  alexsubALTlem3  22062  ustssco  22227  ust0  22232  ustbas2  22238  ustimasn  22241  utopbas  22248  utop2nei  22263  setsmstopn  22492  metustsym  22569  metust  22572  tngtopn  22663  ovoliunlem1  23479  lhop1lem  23986  ig1peu  24141  ig1pdvds  24146  logccv  24619  amgmlem  24926  upgr1e  26218  uspgr1e  26348  shsupcl  28521  shsupunss  28529  shslubi  28568  orthin  28629  h1datomi  28764  mdslj2i  29503  mdslmd1lem1  29508  pwuniss  29691  iundifdifd  29701  difres  29734  fresf1o  29756  metideq  30257  hauseqcn  30262  tpr2rico  30279  esumrnmpt2  30451  esumpfinvallem  30457  esum2d  30476  omssubadd  30683  carsggect  30701  omsmeas  30706  orvcelval  30851  signsply0  30949  cvmlift2lem11  31613  cvmlift2lem12  31614  dfon2lem7  32009  filnetlem3  32691  onsucsuccmpi  32754  dissneqlem  33499  icoreunrn  33518  mblfinlem1  33754  ismblfin  33758  sstotbnd2  33879  dochexmidlem4  37238  lcfrlem38  37355  ismrcd1  37757  eldioph2lem2  37820  rmxyelqirr  37970  hbt  38195  rngunsnply  38238  iocinico  38291  dmtrcl  38428  rntrcl  38429  trrelsuperrel2dg  38457  restuni5  39792  unirnmapsn  39887  limciccioolb  40327  limcrecl  40335  limcicciooub  40343  stoweidlem50  40740  stoweidlem52  40742  stoweidlem53  40743  stoweidlem57  40747  stoweidlem59  40749  fourierdlem50  40846  fourierdlem103  40899  fourierdlem104  40900  pwsal  41008  sge0iun  41109  sge0isum  41117  meadjuni  41147  omessle  41188  zlmodzxzel  42695  lincresunit3  42832  amgmwlem  43113
  Copyright terms: Public domain W3C validator