Theorem sseqtrdi 4023

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 4012	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	sylib 218	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ss 3967

This theorem is referenced by:  sseqtrrdi  4024  3sstr3g  4035  sofld  6206  relrelss  6292  foimacnv  6864  onfununi  8382  hartogslem1  9583  cantnfp1lem3  9721  uniwf  9860  rankeq0b  9901  djuinf  10230  cflecard  10294  fin23lem16  10376  fin23lem41  10393  pwcfsdom  10624  fpwwe2lem12  10683  fpwwe2  10684  canth4  10688  hashbclem  14492  dmtrclfv  15058  zsum  15755  fsumcvg3  15766  incexclem  15873  zprod  15974  ramub1lem1  17065  setsstruct2  17212  imasaddfnlem  17574  imasvscafn  17583  mremre  17648  submre  17649  mreexexlem3d  17690  isacs1i  17701  acsmapd  18600  acsmap2d  18601  ghmqusnsglem1  19299  gsumzoppg  19963  rhmimasubrnglem  20566  subdrgint  20805  primefld  20807  lspsntri  21097  lsppratlem4  21153  lbsextlem3  21163  sraring  21194  evls1maplmhm  22382  distop  23003  elcls  23082  cnpresti  23297  cnprest  23298  cmpcld  23411  cnconn  23431  iunconn  23437  comppfsc  23541  ptuni2  23585  alexsubALTlem3  24058  ustssco  24224  ust0  24229  ustbas2  24235  ustimasn  24238  utopbas  24245  utop2nei  24260  setsmstopn  24491  metustsym  24569  metust  24572  tngtopn  24672  ovoliunlem1  25538  lhop1lem  26053  ig1peu  26215  ig1pdvds  26220  logccv  26706  amgmlem  27034  upgr1e  29131  uspgr1e  29262  shsupcl  31358  shsupunss  31366  shslubi  31405  orthin  31466  h1datomi  31601  mdslj2i  32340  mdslmd1lem1  32345  iundifdifd  32575  iunxpssiun1  32582  difres  32614  fresf1o  32642  suppovss  32691  swrdrndisj  32943  elrgspnlem3  33249  fracf1  33310  idomsubr  33312  nsgmgclem  33440  sradrng  33634  sraidom  33635  resssra  33639  lsssra  33640  zarcmplem  33881  metideq  33893  hauseqcn  33898  tpr2rico  33912  esumrnmpt2  34070  esumpfinvallem  34076  esum2d  34095  omssubadd  34303  carsggect  34321  omsmeas  34326  orvcelval  34472  signsply0  34567  cvmlift2lem11  35319  cvmlift2lem12  35320  dfon2lem7  35791  filnetlem3  36382  onsucsuccmpi  36445  dissneqlem  37342  icoreunrn  37361  ctbssinf  37408  pibt2  37419  mblfinlem1  37665  ismblfin  37669  sstotbnd2  37782  dochexmidlem4  41466  lcfrlem38  41583  rhmqusspan  42187  mhpind  42609  ismrcd1  42714  eldioph2lem2  42777  rmxyelqirrOLD  42927  hbt  43147  rngunsnply  43186  iocinico  43229  dmtrcl  43645  rntrcl  43646  trrelsuperrel2dg  43689  restuni5  45133  unirnmapsn  45224  limciccioolb  45641  limcrecl  45649  limcicciooub  45657  stoweidlem50  46070  stoweidlem52  46072  stoweidlem53  46073  stoweidlem57  46077  stoweidlem59  46079  fourierdlem50  46176  fourierdlem103  46229  fourierdlem104  46230  pwsal  46335  sge0iun  46439  sge0isum  46447  meadjuni  46477  omessle  46518  zlmodzxzel  48276  lincresunit3  48403  amgmwlem  49376