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

Theorem sseqtrdi 4017
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 3996 . 2 (𝐴𝐵𝐴𝐶)
41, 3sylib 220 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wss 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952
This theorem is referenced by:  sseqtrrdi  4018  sofld  6044  relrelss  6124  foimacnv  6632  onfununi  7978  hartogslem1  9006  cantnfp1lem3  9143  uniwf  9248  rankeq0b  9289  djuinf  9614  cflecard  9675  fin23lem16  9757  fin23lem41  9774  pwcfsdom  10005  fpwwe2lem13  10064  fpwwe2  10065  canth4  10069  hashbclem  13811  dmtrclfv  14378  zsum  15075  fsumcvg3  15086  incexclem  15191  zprod  15291  ramub1lem1  16362  setsstruct2  16521  imasaddfnlem  16801  imasvscafn  16810  mremre  16875  submre  16876  mreexexlem3d  16917  isacs1i  16928  acsmapd  17788  acsmap2d  17789  gsumzoppg  19064  subdrgint  19582  primefld  19584  lspsntri  19869  lsppratlem4  19922  lbsextlem3  19932  distop  21603  elcls  21681  cnpresti  21896  cnprest  21897  cmpcld  22010  cnconn  22030  iunconn  22036  comppfsc  22140  ptuni2  22184  alexsubALTlem3  22657  ustssco  22823  ust0  22828  ustbas2  22834  ustimasn  22837  utopbas  22844  utop2nei  22859  setsmstopn  23088  metustsym  23165  metust  23168  tngtopn  23259  ovoliunlem1  24103  lhop1lem  24610  ig1peu  24765  ig1pdvds  24770  logccv  25246  amgmlem  25567  upgr1e  26898  uspgr1e  27026  shsupcl  29115  shsupunss  29123  shslubi  29162  orthin  29223  h1datomi  29358  mdslj2i  30097  mdslmd1lem1  30102  iundifdifd  30313  difres  30350  fresf1o  30376  suppovss  30426  swrdrndisj  30631  sraring  30987  sradrng  30988  metideq  31133  hauseqcn  31138  tpr2rico  31155  esumrnmpt2  31327  esumpfinvallem  31333  esum2d  31352  omssubadd  31558  carsggect  31576  omsmeas  31581  orvcelval  31726  signsply0  31821  cvmlift2lem11  32560  cvmlift2lem12  32561  dfon2lem7  33034  filnetlem3  33728  onsucsuccmpi  33791  dissneqlem  34624  icoreunrn  34643  ctbssinf  34690  pibt2  34701  mblfinlem1  34944  ismblfin  34948  sstotbnd2  35067  dochexmidlem4  38614  lcfrlem38  38731  ismrcd1  39315  eldioph2lem2  39378  rmxyelqirr  39527  hbt  39750  rngunsnply  39793  iocinico  39838  dmtrcl  40007  rntrcl  40008  trrelsuperrel2dg  40036  restuni5  41409  unirnmapsn  41497  limciccioolb  41922  limcrecl  41930  limcicciooub  41938  stoweidlem50  42355  stoweidlem52  42357  stoweidlem53  42358  stoweidlem57  42362  stoweidlem59  42364  fourierdlem50  42461  fourierdlem103  42514  fourierdlem104  42515  pwsal  42620  sge0iun  42721  sge0isum  42729  meadjuni  42759  omessle  42800  zlmodzxzel  44423  lincresunit3  44556  amgmwlem  44923
  Copyright terms: Public domain W3C validator