Theorem sseqtrrid 3982

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 2771	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	1, 3	sseqtrid 3981	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  unissint  4933  resdif  6832  tfrlem5  8354  naddunif  8668  domss2  9112  dffi3  9379  cantnfp1lem3  9637  trcl  9685  tcid  9694  r1ordg  9738  r1sssuc  9743  ackbij1lem15  10204  cfsmolem  10242  fin1a2lem7  10378  wunex2  10711  wuncid  10716  trclfvlb  15035  rtrclreclem2  15086  fsumsplit  15782  o1fsum  15855  fprodsplit  16010  phimullem  16828  vdwlem6  17036  ressinbas  17295  mrcssid  17663  mreexexlem2d  17691  acsfiindd  18599  dirge  18649  symgbasfi  19440  efgredlemf  19802  efgredlemd  19805  gsumzres  19970  gsumzcl2  19971  gsumzf1o  19973  gsumadd  19984  gsumzsplit  19988  gsumsplit2  19990  dprd2da  20105  dmdprdsplit2lem  20108  dmdprdsplit2  20109  dmdprdsplit  20110  dprdsplit  20111  invrpropd  20491  rgspnssid  20690  srhmsubc  20756  issubdrg  20852  lspssid  21075  pjcss  21826  aspssid  21987  psdmul  22289  istopon  23030  sscls  23174  ordtbas  23310  cncls2  23391  tgcmp  23519  cmpfi  23526  1stcfb  23563  1stckgenlem  23671  ptbasfi  23699  ptcnplem  23739  ptuncnv  23925  ptunhmeo  23926  fbasrn  24002  cnflf2  24121  fclscmp  24148  alexsublem  24162  ghmcnp  24233  tsmsgsum  24257  tsmsres  24262  tsmssplit  24270  tsmsxplem1  24271  ustssco  24333  mopnfss  24561  cnmpopc  25048  uniiccdif  25698  uniioombllem3  25705  uniioombllem4  25706  itg2splitlem  25868  itg2split  25869  itgsplit  25956  ellimc2  25997  ellimc3  25999  lhop  26136  itgpowd  26170  plyaddlem1  26331  plymullem1  26332  taylthlem2  26495  mtest  26525  xrlimcnp  27091  fsumharmonic  27134  chtdif  27280  dchrghm  27378  lgsquadlem2  27503  dchrisumlema  27610  dchrisumlem2  27612  dchrisum0lem1b  27637  dchrisum0lem1  27638  pntrlog2bndlem6  27705  pntlemf  27727  precsexlem6  28363  precsexlem7  28364  ltonold  28412  nbupgruvtxres  29666  cyclnumvtx  30058  umgr2adedgwlk  30203  umgr2adedgwlkon  30204  umgr2adedgspth  30206  ex-res  30701  spanss2  31606  mdsymi  32672  cycpmco2lem5  33363  cycpmco2lem6  33364  cycpmco2lem7  33365  cycpmco2  33366  fldgenssid  33549  vietalem  33886  ordtconnlem1  34231  issgon  34430  sssigagen  34452  measiuns  34524  sitgclg  34649  cvmliftlem10  35657  satfsschain  35727  fmlasssuc  35752  satfun  35774  dfttc3gw  36896  rdgssun  37884  ftc1anclem6  38209  heibor1lem  38320  heibor  38332  divrngcl  38468  isdrngo2  38469  igenss  38573  paddunssN  40444  sspadd1  40451  sspadd2  40452  pclssidN  40531  diassdvaN  41696  dochvalr  41993  lcdvbase  42229  nacsfix  43305  isnumbasgrplem2  43693  tfsconcatrnss12  43938  trrelsuperrel2dg  44259  fvilbd  44277  relexp0a  44304  wnefimgd  44749  grumnudlem  44859  icccncfext  46459  iblsplit  46538  dirkeritg  46674  dirkercncflem2  46676  fourierdlem81  46759  fourierdlem89  46767  fourierdlem91  46769  fourierdlem92  46770  fourierdlem111  46789  fouriercn  46804  hspdifhsp  47188  3f1oss1  47667  dfnbgrss  48472  dfnbgrss2  48479  gsumsplit2f  48800  srhmsubcALTV  48945  fdivmpt  49171  fdivpm  49174  refdivpm  49175  mreclat  49626  elpglem2  50341