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

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

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  39344  eldioph2lem2  39407  rmxyelqirr  39556  hbt  39779  rngunsnply  39822  iocinico  39867  dmtrcl  40036  rntrcl  40037  trrelsuperrel2dg  40065  restuni5  41438  unirnmapsn  41526  limciccioolb  41951  limcrecl  41959  limcicciooub  41967  stoweidlem50  42384  stoweidlem52  42386  stoweidlem53  42387  stoweidlem57  42391  stoweidlem59  42393  fourierdlem50  42490  fourierdlem103  42543  fourierdlem104  42544  pwsal  42649  sge0iun  42750  sge0isum  42758  meadjuni  42788  omessle  42829  zlmodzxzel  44452  lincresunit3  44585  amgmwlem  44952