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

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

Proof of Theorem sseqtrdi
StepHypRef Expression
1 sseqtrdi.1 . 2 (𝜑𝐴𝐵)
2 sseqtrdi.2 . . 3 𝐵 = 𝐶
32sseq2i 3947 . 2 (𝐴𝐵𝐴𝐶)
41, 3sylib 221 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wss 3883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-v 3425  df-in 3890  df-ss 3900
This theorem is referenced by:  sseqtrrdi  3969  sofld  6068  relrelss  6154  foimacnv  6700  onfununi  8102  hartogslem1  9188  cantnfp1lem3  9325  uniwf  9465  rankeq0b  9506  djuinf  9832  cflecard  9897  fin23lem16  9979  fin23lem41  9996  pwcfsdom  10227  fpwwe2lem12  10286  fpwwe2  10287  canth4  10291  hashbclem  14049  dmtrclfv  14614  zsum  15315  fsumcvg3  15326  incexclem  15433  zprod  15532  ramub1lem1  16612  setsstruct2  16760  imasaddfnlem  17066  imasvscafn  17075  mremre  17140  submre  17141  mreexexlem3d  17182  isacs1i  17193  acsmapd  18093  acsmap2d  18094  gsumzoppg  19362  subdrgint  19880  primefld  19882  lspsntri  20167  lsppratlem4  20220  lbsextlem3  20230  distop  21924  elcls  22002  cnpresti  22217  cnprest  22218  cmpcld  22331  cnconn  22351  iunconn  22357  comppfsc  22461  ptuni2  22505  alexsubALTlem3  22978  ustssco  23144  ust0  23149  ustbas2  23155  ustimasn  23158  utopbas  23165  utop2nei  23180  setsmstopn  23408  metustsym  23485  metust  23488  tngtopn  23580  ovoliunlem1  24431  lhop1lem  24942  ig1peu  25101  ig1pdvds  25106  logccv  25583  amgmlem  25904  upgr1e  27236  uspgr1e  27364  shsupcl  29451  shsupunss  29459  shslubi  29498  orthin  29559  h1datomi  29694  mdslj2i  30433  mdslmd1lem1  30438  iundifdifd  30652  difres  30690  fresf1o  30717  suppovss  30769  swrdrndisj  30981  nsgmgclem  31342  sraring  31418  sradrng  31419  zarcmplem  31577  metideq  31589  hauseqcn  31594  tpr2rico  31608  esumrnmpt2  31780  esumpfinvallem  31786  esum2d  31805  omssubadd  32011  carsggect  32029  omsmeas  32034  orvcelval  32179  signsply0  32274  cvmlift2lem11  33019  cvmlift2lem12  33020  dfon2lem7  33515  filnetlem3  34340  onsucsuccmpi  34403  dissneqlem  35285  icoreunrn  35304  ctbssinf  35351  pibt2  35362  mblfinlem1  35588  ismblfin  35592  sstotbnd2  35706  dochexmidlem4  39251  lcfrlem38  39368  mhpind  40042  ismrcd1  40271  eldioph2lem2  40334  rmxyelqirr  40483  hbt  40706  rngunsnply  40749  iocinico  40794  dmtrcl  40959  rntrcl  40960  trrelsuperrel2dg  41004  restuni5  42393  unirnmapsn  42475  limciccioolb  42883  limcrecl  42891  limcicciooub  42899  stoweidlem50  43312  stoweidlem52  43314  stoweidlem53  43315  stoweidlem57  43319  stoweidlem59  43321  fourierdlem50  43418  fourierdlem103  43471  fourierdlem104  43472  pwsal  43577  sge0iun  43678  sge0isum  43686  meadjuni  43716  omessle  43757  zlmodzxzel  45410  lincresunit3  45541  amgmwlem  46223
  Copyright terms: Public domain W3C validator