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

Theorem sseqtrdi 4015
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 3994 . 2 (𝐴𝐵𝐴𝐶)
41, 3sylib 220 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wss 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950
This theorem is referenced by:  sseqtrrdi  4016  sofld  6037  relrelss  6117  foimacnv  6625  onfununi  7970  hartogslem1  8998  cantnfp1lem3  9135  uniwf  9240  rankeq0b  9281  djuinf  9606  cflecard  9667  fin23lem16  9749  fin23lem41  9766  pwcfsdom  9997  fpwwe2lem13  10056  fpwwe2  10057  canth4  10061  hashbclem  13802  dmtrclfv  14370  zsum  15067  fsumcvg3  15078  incexclem  15183  zprod  15283  ramub1lem1  16354  setsstruct2  16513  imasaddfnlem  16793  imasvscafn  16802  mremre  16867  submre  16868  mreexexlem3d  16909  isacs1i  16920  acsmapd  17780  acsmap2d  17781  gsumzoppg  19056  subdrgint  19574  primefld  19576  lspsntri  19861  lsppratlem4  19914  lbsextlem3  19924  distop  21595  elcls  21673  cnpresti  21888  cnprest  21889  cmpcld  22002  cnconn  22022  iunconn  22028  comppfsc  22132  ptuni2  22176  alexsubALTlem3  22649  ustssco  22815  ust0  22820  ustbas2  22826  ustimasn  22829  utopbas  22836  utop2nei  22851  setsmstopn  23080  metustsym  23157  metust  23160  tngtopn  23251  ovoliunlem1  24095  lhop1lem  24602  ig1peu  24757  ig1pdvds  24762  logccv  25238  amgmlem  25559  upgr1e  26890  uspgr1e  27018  shsupcl  29107  shsupunss  29115  shslubi  29154  orthin  29215  h1datomi  29350  mdslj2i  30089  mdslmd1lem1  30094  iundifdifd  30305  difres  30342  fresf1o  30368  suppovss  30418  swrdrndisj  30624  sraring  30980  sradrng  30981  metideq  31126  hauseqcn  31131  tpr2rico  31148  esumrnmpt2  31320  esumpfinvallem  31326  esum2d  31345  omssubadd  31551  carsggect  31569  omsmeas  31574  orvcelval  31719  signsply0  31814  cvmlift2lem11  32553  cvmlift2lem12  32554  dfon2lem7  33027  filnetlem3  33721  onsucsuccmpi  33784  dissneqlem  34613  icoreunrn  34632  ctbssinf  34679  pibt2  34690  mblfinlem1  34921  ismblfin  34925  sstotbnd2  35044  dochexmidlem4  38591  lcfrlem38  38708  ismrcd1  39285  eldioph2lem2  39348  rmxyelqirr  39497  hbt  39720  rngunsnply  39763  iocinico  39808  dmtrcl  39977  rntrcl  39978  trrelsuperrel2dg  40006  restuni5  41379  unirnmapsn  41466  limciccioolb  41891  limcrecl  41899  limcicciooub  41907  stoweidlem50  42325  stoweidlem52  42327  stoweidlem53  42328  stoweidlem57  42332  stoweidlem59  42334  fourierdlem50  42431  fourierdlem103  42484  fourierdlem104  42485  pwsal  42590  sge0iun  42691  sge0isum  42699  meadjuni  42729  omessle  42770  zlmodzxzel  44393  lincresunit3  44526  amgmwlem  44893
  Copyright terms: Public domain W3C validator