Theorem sseqtrrid 3970

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	. . 3 ⊢ 𝐵 ⊆ 𝐴
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		sseqtrrid.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
4	2, 3	sseqtrrd 3958	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  unissint  4900  resdif  6720  fimacnvOLD  6930  tfrlem5  8182  domss2  8872  dffi3  9120  cantnfp1lem3  9368  trcl  9417  tcid  9428  r1ordg  9467  r1sssuc  9472  ackbij1lem15  9921  cfsmolem  9957  fin1a2lem7  10093  wunex2  10425  wuncid  10430  trclfvlb  14647  rtrclreclem2  14698  fsumsplit  15381  o1fsum  15453  fprodsplit  15604  phimullem  16408  vdwlem6  16615  ressinbas  16881  mrcssid  17243  mreexexlem2d  17271  acsfiindd  18186  dirge  18236  symgbasfi  18901  efgredlemf  19262  efgredlemd  19265  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumadd  19439  gsumzsplit  19443  gsumsplit2  19445  dprd2da  19560  dmdprdsplit2lem  19563  dmdprdsplit2  19564  dmdprdsplit  19565  dprdsplit  19566  invrpropd  19855  issubdrg  19964  lspssid  20162  pjcss  20833  aspssid  20992  istopon  21969  sscls  22115  ordtbas  22251  cncls2  22332  tgcmp  22460  cmpfi  22467  1stcfb  22504  1stckgenlem  22612  ptbasfi  22640  ptcnplem  22680  ptuncnv  22866  ptunhmeo  22867  fbasrn  22943  cnflf2  23062  fclscmp  23089  alexsublem  23103  ghmcnp  23174  tsmsgsum  23198  tsmsres  23203  tsmssplit  23211  tsmsxplem1  23212  ustssco  23274  mopnfss  23504  cnmpopc  23997  uniiccdif  24647  uniioombllem3  24654  uniioombllem4  24655  itg2splitlem  24818  itg2split  24819  itgsplit  24905  ellimc2  24946  ellimc3  24948  lhop  25085  itgpowd  25119  plyaddlem1  25279  plymullem1  25280  taylthlem2  25438  mtest  25468  xrlimcnp  26023  fsumharmonic  26066  chtdif  26212  dchrghm  26309  lgsquadlem2  26434  dchrisumlema  26541  dchrisumlem2  26543  dchrisum0lem1b  26568  dchrisum0lem1  26569  pntrlog2bndlem6  26636  pntlemf  26658  nbupgruvtxres  27677  umgr2adedgwlk  28211  umgr2adedgwlkon  28212  umgr2adedgspth  28214  ex-res  28706  spanss2  29608  mdsymi  30674  padct  30956  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  ordtconnlem1  31776  issgon  31991  sssigagen  32013  measiuns  32085  sitgclg  32209  cvmliftlem10  33156  satfsschain  33226  fmlasssuc  33251  satfun  33273  rdgssun  35476  ftc1anclem6  35782  heibor1lem  35894  heibor  35906  divrngcl  36042  isdrngo2  36043  igenss  36147  paddunssN  37749  sspadd1  37756  sspadd2  37757  pclssidN  37836  diassdvaN  39001  dochvalr  39298  lcdvbase  39534  nacsfix  40450  isnumbasgrplem2  40845  rgspnssid  40911  trrelsuperrel2dg  41168  fvilbd  41186  relexp0a  41213  wnefimgd  41661  grumnudlem  41792  icccncfext  43318  iblsplit  43397  dirkeritg  43533  dirkercncflem2  43535  fourierdlem81  43618  fourierdlem89  43626  fourierdlem91  43628  fourierdlem92  43629  fourierdlem111  43648  fouriercn  43663  hspdifhsp  44044  gsumsplit2f  45262  srhmsubc  45522  srhmsubcALTV  45540  fdivmpt  45774  fdivpm  45777  refdivpm  45778  mreclat  46171  elpglem2  46303