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

Theorem syl6sseq 3684
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 3663 . 2 (𝐴𝐵𝐴𝐶)
41, 3sylib 208 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  syl6sseqr  3685  sofld  5616  relrelss  5697  foimacnv  6192  onfununi  7483  hartogslem1  8488  cantnfp1lem3  8615  uniwf  8720  rankeq0b  8761  cflecard  9113  fin23lem16  9195  fin23lem41  9212  pwcfsdom  9443  fpwwe2lem13  9502  fpwwe2  9503  canth4  9507  hashbclem  13274  dmtrclfv  13803  zsum  14493  fsumcvg3  14504  incexclem  14612  zprod  14711  ramub1lem1  15777  setsstruct2  15943  imasaddfnlem  16235  imasvscafn  16244  mremre  16311  submre  16312  mreexexlem3d  16353  isacs1i  16365  acsmapd  17225  acsmap2d  17226  gsumzoppg  18390  lspsntri  19145  lsppratlem4  19198  lbsextlem3  19208  distop  20847  elcls  20925  cnpresti  21140  cnprest  21141  cmpcld  21253  cnconn  21273  iunconn  21279  comppfsc  21383  ptuni2  21427  alexsubALTlem3  21900  ustssco  22065  ust0  22070  ustbas2  22076  ustimasn  22079  utopbas  22086  utop2nei  22101  setsmstopn  22330  metustsym  22407  metust  22410  tngtopn  22501  ovoliunlem1  23316  lhop1lem  23821  ig1peu  23976  ig1pdvds  23981  logccv  24454  amgmlem  24761  upgr1e  26053  uspgr1e  26181  shsupcl  28325  shsupunss  28333  shslubi  28372  orthin  28433  h1datomi  28568  mdslj2i  29307  mdslmd1lem1  29312  pwuniss  29496  iundifdifd  29506  difres  29539  fresf1o  29561  metideq  30064  hauseqcn  30069  tpr2rico  30086  esumrnmpt2  30258  esumpfinvallem  30264  esum2d  30283  omssubadd  30490  carsggect  30508  omsmeas  30513  orvcelval  30658  signsply0  30756  cvmlift2lem11  31421  cvmlift2lem12  31422  dfon2lem7  31818  filnetlem3  32500  onsucsuccmpi  32567  dissneqlem  33317  icoreunrn  33337  mblfinlem1  33576  ismblfin  33580  sstotbnd2  33703  dochexmidlem4  37069  lcfrlem38  37186  ismrcd1  37578  eldioph2lem2  37641  rmxyelqirr  37792  hbt  38017  rngunsnply  38060  iocinico  38114  dmtrcl  38251  rntrcl  38252  trrelsuperrel2dg  38280  restuni5  39620  unirnmapsn  39720  limciccioolb  40171  limcrecl  40179  limcicciooub  40187  stoweidlem50  40585  stoweidlem52  40587  stoweidlem53  40588  stoweidlem57  40592  stoweidlem59  40594  fourierdlem50  40691  fourierdlem103  40744  fourierdlem104  40745  pwsal  40853  sge0iun  40954  sge0isum  40962  meadjuni  40992  omessle  41033  zlmodzxzel  42458  lincresunit3  42595  amgmwlem  42876
  Copyright terms: Public domain W3C validator