Theorem sseqtrrid 3977

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  unissint  4927  resdif  6795  tfrlem5  8311  naddunif  8621  domss2  9064  dffi3  9334  cantnfp1lem3  9589  trcl  9637  tcid  9646  r1ordg  9690  r1sssuc  9695  ackbij1lem15  10143  cfsmolem  10180  fin1a2lem7  10316  wunex2  10649  wuncid  10654  trclfvlb  14931  rtrclreclem2  14982  fsumsplit  15664  o1fsum  15736  fprodsplit  15889  phimullem  16706  vdwlem6  16914  ressinbas  17172  mrcssid  17540  mreexexlem2d  17568  acsfiindd  18476  dirge  18526  symgbasfi  19308  efgredlemf  19670  efgredlemd  19673  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumadd  19852  gsumzsplit  19856  gsumsplit2  19858  dprd2da  19973  dmdprdsplit2lem  19976  dmdprdsplit2  19977  dmdprdsplit  19978  dprdsplit  19979  invrpropd  20354  rgspnssid  20547  srhmsubc  20613  issubdrg  20713  lspssid  20936  pjcss  21671  aspssid  21833  psdmul  22109  istopon  22856  sscls  23000  ordtbas  23136  cncls2  23217  tgcmp  23345  cmpfi  23352  1stcfb  23389  1stckgenlem  23497  ptbasfi  23525  ptcnplem  23565  ptuncnv  23751  ptunhmeo  23752  fbasrn  23828  cnflf2  23947  fclscmp  23974  alexsublem  23988  ghmcnp  24059  tsmsgsum  24083  tsmsres  24088  tsmssplit  24096  tsmsxplem1  24097  ustssco  24159  mopnfss  24387  cnmpopc  24878  uniiccdif  25535  uniioombllem3  25542  uniioombllem4  25543  itg2splitlem  25705  itg2split  25706  itgsplit  25793  ellimc2  25834  ellimc3  25836  lhop  25977  itgpowd  26013  plyaddlem1  26174  plymullem1  26175  taylthlem2  26338  taylthlem2OLD  26339  mtest  26369  xrlimcnp  26934  fsumharmonic  26978  chtdif  27124  dchrghm  27223  lgsquadlem2  27348  dchrisumlema  27455  dchrisumlem2  27457  dchrisum0lem1b  27482  dchrisum0lem1  27483  pntrlog2bndlem6  27550  pntlemf  27572  precsexlem6  28208  precsexlem7  28209  ltonold  28257  nbupgruvtxres  29480  cyclnumvtx  29873  umgr2adedgwlk  30018  umgr2adedgwlkon  30019  umgr2adedgspth  30021  ex-res  30516  spanss2  31420  mdsymi  32486  padct  32797  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  fldgenssid  33395  vietalem  33735  ordtconnlem1  34081  issgon  34280  sssigagen  34302  measiuns  34374  sitgclg  34499  cvmliftlem10  35488  satfsschain  35558  fmlasssuc  35583  satfun  35605  rdgssun  37579  ftc1anclem6  37895  heibor1lem  38006  heibor  38018  divrngcl  38154  isdrngo2  38155  igenss  38259  paddunssN  40064  sspadd1  40071  sspadd2  40072  pclssidN  40151  diassdvaN  41316  dochvalr  41613  lcdvbase  41849  nacsfix  42950  isnumbasgrplem2  43342  tfsconcatrnss12  43587  trrelsuperrel2dg  43908  fvilbd  43926  relexp0a  43953  wnefimgd  44398  grumnudlem  44522  icccncfext  46127  iblsplit  46206  dirkeritg  46342  dirkercncflem2  46344  fourierdlem81  46427  fourierdlem89  46435  fourierdlem91  46437  fourierdlem92  46438  fourierdlem111  46457  fouriercn  46472  hspdifhsp  46856  3f1oss1  47317  dfnbgrss  48094  dfnbgrss2  48101  gsumsplit2f  48422  srhmsubcALTV  48567  fdivmpt  48782  fdivpm  48785  refdivpm  48786  mreclat  49238  elpglem2  49953