Theorem sseqtrrid 3965

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  unissint  4909  resdif  6795  tfrlem5  8316  naddunif  8626  domss2  9071  dffi3  9341  cantnfp1lem3  9599  trcl  9647  tcid  9656  r1ordg  9700  r1sssuc  9705  ackbij1lem15  10153  cfsmolem  10190  fin1a2lem7  10326  wunex2  10659  wuncid  10664  trclfvlb  14968  rtrclreclem2  15019  fsumsplit  15701  o1fsum  15774  fprodsplit  15929  phimullem  16747  vdwlem6  16955  ressinbas  17213  mrcssid  17581  mreexexlem2d  17609  acsfiindd  18517  dirge  18567  symgbasfi  19352  efgredlemf  19714  efgredlemd  19717  gsumzres  19882  gsumzcl2  19883  gsumzf1o  19885  gsumadd  19896  gsumzsplit  19900  gsumsplit2  19902  dprd2da  20017  dmdprdsplit2lem  20020  dmdprdsplit2  20021  dmdprdsplit  20022  dprdsplit  20023  invrpropd  20396  rgspnssid  20593  srhmsubc  20659  issubdrg  20759  lspssid  20982  pjcss  21698  aspssid  21859  psdmul  22161  istopon  22902  sscls  23046  ordtbas  23182  cncls2  23263  tgcmp  23391  cmpfi  23398  1stcfb  23435  1stckgenlem  23543  ptbasfi  23571  ptcnplem  23611  ptuncnv  23797  ptunhmeo  23798  fbasrn  23874  cnflf2  23993  fclscmp  24020  alexsublem  24034  ghmcnp  24105  tsmsgsum  24129  tsmsres  24134  tsmssplit  24142  tsmsxplem1  24143  ustssco  24205  mopnfss  24433  cnmpopc  24920  uniiccdif  25570  uniioombllem3  25577  uniioombllem4  25578  itg2splitlem  25740  itg2split  25741  itgsplit  25828  ellimc2  25869  ellimc3  25871  lhop  26008  itgpowd  26042  plyaddlem1  26203  plymullem1  26204  taylthlem2  26364  mtest  26394  xrlimcnp  26957  fsumharmonic  27000  chtdif  27146  dchrghm  27244  lgsquadlem2  27369  dchrisumlema  27476  dchrisumlem2  27478  dchrisum0lem1b  27503  dchrisum0lem1  27504  pntrlog2bndlem6  27571  pntlemf  27593  precsexlem6  28229  precsexlem7  28230  ltonold  28278  nbupgruvtxres  29501  cyclnumvtx  29893  umgr2adedgwlk  30038  umgr2adedgwlkon  30039  umgr2adedgspth  30041  ex-res  30536  spanss2  31441  mdsymi  32507  cycpmco2lem5  33218  cycpmco2lem6  33219  cycpmco2lem7  33220  cycpmco2  33221  fldgenssid  33404  vietalem  33770  ordtconnlem1  34115  issgon  34314  sssigagen  34336  measiuns  34408  sitgclg  34533  cvmliftlem10  35529  satfsschain  35599  fmlasssuc  35624  satfun  35646  dfttc3gw  36758  rdgssun  37747  ftc1anclem6  38072  heibor1lem  38183  heibor  38195  divrngcl  38331  isdrngo2  38332  igenss  38436  paddunssN  40307  sspadd1  40314  sspadd2  40315  pclssidN  40394  diassdvaN  41559  dochvalr  41856  lcdvbase  42092  nacsfix  43168  isnumbasgrplem2  43556  tfsconcatrnss12  43801  trrelsuperrel2dg  44122  fvilbd  44140  relexp0a  44167  wnefimgd  44612  grumnudlem  44736  icccncfext  46337  iblsplit  46416  dirkeritg  46552  dirkercncflem2  46554  fourierdlem81  46637  fourierdlem89  46645  fourierdlem91  46647  fourierdlem92  46648  fourierdlem111  46667  fouriercn  46682  hspdifhsp  47066  3f1oss1  47545  dfnbgrss  48350  dfnbgrss2  48357  gsumsplit2f  48678  srhmsubcALTV  48823  fdivmpt  49038  fdivpm  49041  refdivpm  49042  mreclat  49494  elpglem2  50209