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

Theorem sseqtrdi 3999
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 3978 . 2 (𝐴𝐵𝐴𝐶)
41, 3sylib 217 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  sseqtrrdi  4000  sofld  6144  relrelss  6230  foimacnv  6806  onfununi  8292  hartogslem1  9485  cantnfp1lem3  9623  uniwf  9762  rankeq0b  9803  djuinf  10131  cflecard  10196  fin23lem16  10278  fin23lem41  10295  pwcfsdom  10526  fpwwe2lem12  10585  fpwwe2  10586  canth4  10590  hashbclem  14356  dmtrclfv  14910  zsum  15610  fsumcvg3  15621  incexclem  15728  zprod  15827  ramub1lem1  16905  setsstruct2  17053  imasaddfnlem  17417  imasvscafn  17426  mremre  17491  submre  17492  mreexexlem3d  17533  isacs1i  17544  acsmapd  18450  acsmap2d  18451  gsumzoppg  19728  subdrgint  20286  primefld  20288  lspsntri  20574  lsppratlem4  20627  lbsextlem3  20637  distop  22361  elcls  22440  cnpresti  22655  cnprest  22656  cmpcld  22769  cnconn  22789  iunconn  22795  comppfsc  22899  ptuni2  22943  alexsubALTlem3  23416  ustssco  23582  ust0  23587  ustbas2  23593  ustimasn  23596  utopbas  23603  utop2nei  23618  setsmstopn  23849  metustsym  23927  metust  23930  tngtopn  24030  ovoliunlem1  24882  lhop1lem  25393  ig1peu  25552  ig1pdvds  25557  logccv  26034  amgmlem  26355  upgr1e  28106  uspgr1e  28234  shsupcl  30322  shsupunss  30330  shslubi  30369  orthin  30430  h1datomi  30565  mdslj2i  31304  mdslmd1lem1  31309  iundifdifd  31522  difres  31560  fresf1o  31587  suppovss  31640  swrdrndisj  31853  nsgmgclem  32229  sraring  32326  sradrng  32327  zarcmplem  32502  metideq  32514  hauseqcn  32519  tpr2rico  32533  esumrnmpt2  32707  esumpfinvallem  32713  esum2d  32732  omssubadd  32940  carsggect  32958  omsmeas  32963  orvcelval  33108  signsply0  33203  cvmlift2lem11  33947  cvmlift2lem12  33948  dfon2lem7  34403  filnetlem3  34881  onsucsuccmpi  34944  dissneqlem  35840  icoreunrn  35859  ctbssinf  35906  pibt2  35917  mblfinlem1  36144  ismblfin  36148  sstotbnd2  36262  dochexmidlem4  39955  lcfrlem38  40072  mhpind  40798  ismrcd1  41050  eldioph2lem2  41113  rmxyelqirrOLD  41263  hbt  41486  rngunsnply  41529  iocinico  41575  dmtrcl  41973  rntrcl  41974  trrelsuperrel2dg  42017  restuni5  43407  unirnmapsn  43509  limciccioolb  43936  limcrecl  43944  limcicciooub  43952  stoweidlem50  44365  stoweidlem52  44367  stoweidlem53  44368  stoweidlem57  44372  stoweidlem59  44374  fourierdlem50  44471  fourierdlem103  44524  fourierdlem104  44525  pwsal  44630  sge0iun  44734  sge0isum  44742  meadjuni  44772  omessle  44813  zlmodzxzel  46505  lincresunit3  46636  amgmwlem  47323
  Copyright terms: Public domain W3C validator