Theorem sseqtrdi 3987

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

Step	Hyp	Ref	Expression
1		sseqtrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrdi.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	sseq2i 3976	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	sylib 218	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  sseqtrrdi  3988  3sstr3g  3999  sofld  6160  relrelss  6246  foimacnv  6817  onfununi  8310  hartogslem1  9495  cantnfp1lem3  9633  uniwf  9772  rankeq0b  9813  djuinf  10142  cflecard  10206  fin23lem16  10288  fin23lem41  10305  pwcfsdom  10536  fpwwe2lem12  10595  fpwwe2  10596  canth4  10600  hashbclem  14417  dmtrclfv  14984  zsum  15684  fsumcvg3  15695  incexclem  15802  zprod  15903  ramub1lem1  16997  setsstruct2  17144  imasaddfnlem  17491  imasvscafn  17500  mremre  17565  submre  17566  mreexexlem3d  17607  isacs1i  17618  acsmapd  18513  acsmap2d  18514  ghmqusnsglem1  19212  gsumzoppg  19874  rhmimasubrnglem  20474  subdrgint  20712  primefld  20714  lspsntri  21004  lsppratlem4  21060  lbsextlem3  21070  sraring  21093  evls1maplmhm  22264  distop  22882  elcls  22960  cnpresti  23175  cnprest  23176  cmpcld  23289  cnconn  23309  iunconn  23315  comppfsc  23419  ptuni2  23463  alexsubALTlem3  23936  ustssco  24102  ust0  24107  ustbas2  24113  ustimasn  24116  utopbas  24123  utop2nei  24138  setsmstopn  24366  metustsym  24443  metust  24446  tngtopn  24538  ovoliunlem1  25403  lhop1lem  25918  ig1peu  26080  ig1pdvds  26085  logccv  26572  amgmlem  26900  upgr1e  29040  uspgr1e  29171  shsupcl  31267  shsupunss  31275  shslubi  31314  orthin  31375  h1datomi  31510  mdslj2i  32249  mdslmd1lem1  32254  iundifdifd  32490  iunxpssiun1  32497  difres  32529  fresf1o  32555  suppovss  32604  swrdrndisj  32879  elrgspnlem3  33195  fracf1  33257  idomsubr  33259  nsgmgclem  33382  ressply1evls1  33534  sradrng  33578  sraidom  33579  resssra  33583  lsssra  33584  zarcmplem  33871  metideq  33883  hauseqcn  33888  tpr2rico  33902  esumrnmpt2  34058  esumpfinvallem  34064  esum2d  34083  omssubadd  34291  carsggect  34309  omsmeas  34314  orvcelval  34460  signsply0  34542  cvmlift2lem11  35300  cvmlift2lem12  35301  dfon2lem7  35777  filnetlem3  36368  onsucsuccmpi  36431  dissneqlem  37328  icoreunrn  37347  ctbssinf  37394  pibt2  37405  mblfinlem1  37651  ismblfin  37655  sstotbnd2  37768  dochexmidlem4  41457  lcfrlem38  41574  rhmqusspan  42173  mhpind  42582  ismrcd1  42686  eldioph2lem2  42749  rmxyelqirrOLD  42899  hbt  43119  rngunsnply  43158  iocinico  43201  dmtrcl  43616  rntrcl  43617  trrelsuperrel2dg  43660  restuni5  45117  unirnmapsn  45208  limciccioolb  45619  limcrecl  45627  limcicciooub  45635  stoweidlem50  46048  stoweidlem52  46050  stoweidlem53  46051  stoweidlem57  46055  stoweidlem59  46057  fourierdlem50  46154  fourierdlem103  46207  fourierdlem104  46208  pwsal  46313  sge0iun  46417  sge0isum  46425  meadjuni  46455  omessle  46496  uhgrimprop  47889  zlmodzxzel  48340  lincresunit3  48467  amgmwlem  49788