Theorem sseqtrrid 3990

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sseqtrrid.1	⊢ 𝐵 ⊆ 𝐴
sseqtrrid.2	⊢ (𝜑 → 𝐶 = 𝐴)

Assertion

Ref	Expression
sseqtrrid	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem sseqtrrid

Step	Hyp	Ref	Expression
1		sseqtrrid.1	. 2 ⊢ 𝐵 ⊆ 𝐴
2		sseqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3	2	eqcomd 2735	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	1, 3	sseqtrid 3989	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:  unissint  4936  resdif  6821  tfrlem5  8348  naddunif  8657  domss2  9100  dffi3  9382  cantnfp1lem3  9633  trcl  9681  tcid  9692  r1ordg  9731  r1sssuc  9736  ackbij1lem15  10186  cfsmolem  10223  fin1a2lem7  10359  wunex2  10691  wuncid  10696  trclfvlb  14974  rtrclreclem2  15025  fsumsplit  15707  o1fsum  15779  fprodsplit  15932  phimullem  16749  vdwlem6  16957  ressinbas  17215  mrcssid  17578  mreexexlem2d  17606  acsfiindd  18512  dirge  18562  symgbasfi  19309  efgredlemf  19671  efgredlemd  19674  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumadd  19853  gsumzsplit  19857  gsumsplit2  19859  dprd2da  19974  dmdprdsplit2lem  19977  dmdprdsplit2  19978  dmdprdsplit  19979  dprdsplit  19980  invrpropd  20327  rgspnssid  20523  srhmsubc  20589  issubdrg  20689  lspssid  20891  pjcss  21625  aspssid  21787  psdmul  22053  istopon  22799  sscls  22943  ordtbas  23079  cncls2  23160  tgcmp  23288  cmpfi  23295  1stcfb  23332  1stckgenlem  23440  ptbasfi  23468  ptcnplem  23508  ptuncnv  23694  ptunhmeo  23695  fbasrn  23771  cnflf2  23890  fclscmp  23917  alexsublem  23931  ghmcnp  24002  tsmsgsum  24026  tsmsres  24031  tsmssplit  24039  tsmsxplem1  24040  ustssco  24102  mopnfss  24331  cnmpopc  24822  uniiccdif  25479  uniioombllem3  25486  uniioombllem4  25487  itg2splitlem  25649  itg2split  25650  itgsplit  25737  ellimc2  25778  ellimc3  25780  lhop  25921  itgpowd  25957  plyaddlem1  26118  plymullem1  26119  taylthlem2  26282  taylthlem2OLD  26283  mtest  26313  xrlimcnp  26878  fsumharmonic  26922  chtdif  27068  dchrghm  27167  lgsquadlem2  27292  dchrisumlema  27399  dchrisumlem2  27401  dchrisum0lem1b  27426  dchrisum0lem1  27427  pntrlog2bndlem6  27494  pntlemf  27516  precsexlem6  28114  precsexlem7  28115  sltonold  28162  nbupgruvtxres  29334  cyclnumvtx  29730  umgr2adedgwlk  29875  umgr2adedgwlkon  29876  umgr2adedgspth  29878  ex-res  30370  spanss2  31274  mdsymi  32340  padct  32643  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  fldgenssid  33263  ordtconnlem1  33914  issgon  34113  sssigagen  34135  measiuns  34207  sitgclg  34333  cvmliftlem10  35281  satfsschain  35351  fmlasssuc  35376  satfun  35398  rdgssun  37366  ftc1anclem6  37692  heibor1lem  37803  heibor  37815  divrngcl  37951  isdrngo2  37952  igenss  38056  paddunssN  39802  sspadd1  39809  sspadd2  39810  pclssidN  39889  diassdvaN  41054  dochvalr  41351  lcdvbase  41587  nacsfix  42700  isnumbasgrplem2  43093  tfsconcatrnss12  43338  trrelsuperrel2dg  43660  fvilbd  43678  relexp0a  43705  wnefimgd  44150  grumnudlem  44274  icccncfext  45885  iblsplit  45964  dirkeritg  46100  dirkercncflem2  46102  fourierdlem81  46185  fourierdlem89  46193  fourierdlem91  46195  fourierdlem92  46196  fourierdlem111  46215  fouriercn  46230  hspdifhsp  46614  3f1oss1  47076  dfnbgrss  47852  dfnbgrss2  47859  gsumsplit2f  48168  srhmsubcALTV  48313  fdivmpt  48529  fdivpm  48532  refdivpm  48533  mreclat  48985  elpglem2  49701