Theorem sseqtrrid 3979

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  unissint  4929  resdif  6824  tfrlem5  8345  naddunif  8659  domss2  9104  dffi3  9374  cantnfp1lem3  9632  trcl  9680  tcid  9689  r1ordg  9733  r1sssuc  9738  ackbij1lem15  10186  cfsmolem  10224  fin1a2lem7  10360  wunex2  10693  wuncid  10698  trclfvlb  15018  rtrclreclem2  15069  fsumsplit  15751  o1fsum  15824  fprodsplit  15979  phimullem  16797  vdwlem6  17005  ressinbas  17264  mrcssid  17632  mreexexlem2d  17660  acsfiindd  18568  dirge  18618  symgbasfi  19402  efgredlemf  19764  efgredlemd  19767  gsumzres  19932  gsumzcl2  19933  gsumzf1o  19935  gsumadd  19946  gsumzsplit  19950  gsumsplit2  19952  dprd2da  20067  dmdprdsplit2lem  20070  dmdprdsplit2  20071  dmdprdsplit  20072  dprdsplit  20073  invrpropd  20446  rgspnssid  20643  srhmsubc  20709  issubdrg  20809  lspssid  21032  pjcss  21748  aspssid  21909  psdmul  22211  istopon  22952  sscls  23096  ordtbas  23232  cncls2  23313  tgcmp  23441  cmpfi  23448  1stcfb  23485  1stckgenlem  23593  ptbasfi  23621  ptcnplem  23661  ptuncnv  23847  ptunhmeo  23848  fbasrn  23924  cnflf2  24043  fclscmp  24070  alexsublem  24084  ghmcnp  24155  tsmsgsum  24179  tsmsres  24184  tsmssplit  24192  tsmsxplem1  24193  ustssco  24255  mopnfss  24483  cnmpopc  24970  uniiccdif  25620  uniioombllem3  25627  uniioombllem4  25628  itg2splitlem  25790  itg2split  25791  itgsplit  25878  ellimc2  25919  ellimc3  25921  lhop  26058  itgpowd  26092  plyaddlem1  26253  plymullem1  26254  taylthlem2  26414  mtest  26444  xrlimcnp  27010  fsumharmonic  27053  chtdif  27199  dchrghm  27297  lgsquadlem2  27422  dchrisumlema  27529  dchrisumlem2  27531  dchrisum0lem1b  27556  dchrisum0lem1  27557  pntrlog2bndlem6  27624  pntlemf  27646  precsexlem6  28282  precsexlem7  28283  ltonold  28331  nbupgruvtxres  29554  cyclnumvtx  29946  umgr2adedgwlk  30091  umgr2adedgwlkon  30092  umgr2adedgspth  30094  ex-res  30589  spanss2  31494  mdsymi  32560  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmco2  33274  fldgenssid  33461  vietalem  33837  ordtconnlem1  34182  issgon  34381  sssigagen  34403  measiuns  34475  sitgclg  34600  cvmliftlem10  35608  satfsschain  35678  fmlasssuc  35703  satfun  35725  dfttc3gw  36847  rdgssun  37836  ftc1anclem6  38161  heibor1lem  38272  heibor  38284  divrngcl  38420  isdrngo2  38421  igenss  38525  paddunssN  40396  sspadd1  40403  sspadd2  40404  pclssidN  40483  diassdvaN  41648  dochvalr  41945  lcdvbase  42181  nacsfix  43257  isnumbasgrplem2  43645  tfsconcatrnss12  43890  trrelsuperrel2dg  44211  fvilbd  44229  relexp0a  44256  wnefimgd  44701  grumnudlem  44825  icccncfext  46425  iblsplit  46504  dirkeritg  46640  dirkercncflem2  46642  fourierdlem81  46725  fourierdlem89  46733  fourierdlem91  46735  fourierdlem92  46736  fourierdlem111  46755  fouriercn  46770  hspdifhsp  47154  3f1oss1  47633  dfnbgrss  48438  dfnbgrss2  48445  gsumsplit2f  48766  srhmsubcALTV  48911  fdivmpt  49126  fdivpm  49129  refdivpm  49130  mreclat  49582  elpglem2  50297