Theorem sseqtrrid 4027

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  unissint  4966  resdif  6844  fimacnvOLD  7062  tfrlem5  8375  naddunif  8688  domss2  9132  dffi3  9422  cantnfp1lem3  9671  trcl  9719  tcid  9730  r1ordg  9769  r1sssuc  9774  ackbij1lem15  10225  cfsmolem  10261  fin1a2lem7  10397  wunex2  10729  wuncid  10734  trclfvlb  14952  rtrclreclem2  15003  fsumsplit  15684  o1fsum  15756  fprodsplit  15907  phimullem  16711  vdwlem6  16918  ressinbas  17189  mrcssid  17560  mreexexlem2d  17588  acsfiindd  18508  dirge  18558  symgbasfi  19288  efgredlemf  19651  efgredlemd  19654  gsumzres  19819  gsumzcl2  19820  gsumzf1o  19822  gsumadd  19833  gsumzsplit  19837  gsumsplit2  19839  dprd2da  19954  dmdprdsplit2lem  19957  dmdprdsplit2  19958  dmdprdsplit  19959  dprdsplit  19960  invrpropd  20310  srhmsubc  20566  issubdrg  20621  lspssid  20822  pjcss  21579  aspssid  21740  istopon  22736  sscls  22882  ordtbas  23018  cncls2  23099  tgcmp  23227  cmpfi  23234  1stcfb  23271  1stckgenlem  23379  ptbasfi  23407  ptcnplem  23447  ptuncnv  23633  ptunhmeo  23634  fbasrn  23710  cnflf2  23829  fclscmp  23856  alexsublem  23870  ghmcnp  23941  tsmsgsum  23965  tsmsres  23970  tsmssplit  23978  tsmsxplem1  23979  ustssco  24041  mopnfss  24271  cnmpopc  24771  uniiccdif  25429  uniioombllem3  25436  uniioombllem4  25437  itg2splitlem  25600  itg2split  25601  itgsplit  25687  ellimc2  25728  ellimc3  25730  lhop  25871  itgpowd  25907  plyaddlem1  26067  plymullem1  26068  taylthlem2  26227  mtest  26257  xrlimcnp  26816  fsumharmonic  26860  chtdif  27006  dchrghm  27105  lgsquadlem2  27230  dchrisumlema  27337  dchrisumlem2  27339  dchrisum0lem1b  27364  dchrisum0lem1  27365  pntrlog2bndlem6  27432  pntlemf  27454  precsexlem6  28026  precsexlem7  28027  sltonold  28069  nbupgruvtxres  29133  umgr2adedgwlk  29668  umgr2adedgwlkon  29669  umgr2adedgspth  29671  ex-res  30163  spanss2  31067  mdsymi  32133  padct  32413  cycpmco2lem5  32757  cycpmco2lem6  32758  cycpmco2lem7  32759  cycpmco2  32760  fldgenssid  32869  ordtconnlem1  33393  issgon  33610  sssigagen  33632  measiuns  33704  sitgclg  33830  cvmliftlem10  34774  satfsschain  34844  fmlasssuc  34869  satfun  34891  gg-taylthlem2  35657  rdgssun  36749  ftc1anclem6  37056  heibor1lem  37167  heibor  37179  divrngcl  37315  isdrngo2  37316  igenss  37420  paddunssN  39169  sspadd1  39176  sspadd2  39177  pclssidN  39256  diassdvaN  40421  dochvalr  40718  lcdvbase  40954  nacsfix  41939  isnumbasgrplem2  42335  rgspnssid  42401  tfsconcatrnss12  42588  trrelsuperrel2dg  42911  fvilbd  42929  relexp0a  42956  wnefimgd  43402  grumnudlem  43533  icccncfext  45088  iblsplit  45167  dirkeritg  45303  dirkercncflem2  45305  fourierdlem81  45388  fourierdlem89  45396  fourierdlem91  45398  fourierdlem92  45399  fourierdlem111  45418  fouriercn  45433  hspdifhsp  45817  gsumsplit2f  47043  srhmsubcALTV  47188  fdivmpt  47414  fdivpm  47417  refdivpm  47418  mreclat  47810  elpglem2  47945