Theorem sseqtrrid 4034

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  unissint  4975  resdif  6853  fimacnvOLD  7071  tfrlem5  8382  naddunif  8694  domss2  9138  dffi3  9428  cantnfp1lem3  9677  trcl  9725  tcid  9736  r1ordg  9775  r1sssuc  9780  ackbij1lem15  10231  cfsmolem  10267  fin1a2lem7  10403  wunex2  10735  wuncid  10740  trclfvlb  14959  rtrclreclem2  15010  fsumsplit  15691  o1fsum  15763  fprodsplit  15914  phimullem  16716  vdwlem6  16923  ressinbas  17194  mrcssid  17565  mreexexlem2d  17593  acsfiindd  18510  dirge  18560  symgbasfi  19287  efgredlemf  19650  efgredlemd  19653  gsumzres  19818  gsumzcl2  19819  gsumzf1o  19821  gsumadd  19832  gsumzsplit  19836  gsumsplit2  19838  dprd2da  19953  dmdprdsplit2lem  19956  dmdprdsplit2  19957  dmdprdsplit  19958  dprdsplit  19959  invrpropd  20309  issubdrg  20544  lspssid  20740  pjcss  21490  aspssid  21651  istopon  22634  sscls  22780  ordtbas  22916  cncls2  22997  tgcmp  23125  cmpfi  23132  1stcfb  23169  1stckgenlem  23277  ptbasfi  23305  ptcnplem  23345  ptuncnv  23531  ptunhmeo  23532  fbasrn  23608  cnflf2  23727  fclscmp  23754  alexsublem  23768  ghmcnp  23839  tsmsgsum  23863  tsmsres  23868  tsmssplit  23876  tsmsxplem1  23877  ustssco  23939  mopnfss  24169  cnmpopc  24669  uniiccdif  25327  uniioombllem3  25334  uniioombllem4  25335  itg2splitlem  25498  itg2split  25499  itgsplit  25585  ellimc2  25626  ellimc3  25628  lhop  25768  itgpowd  25802  plyaddlem1  25962  plymullem1  25963  taylthlem2  26122  mtest  26152  xrlimcnp  26709  fsumharmonic  26752  chtdif  26898  dchrghm  26995  lgsquadlem2  27120  dchrisumlema  27227  dchrisumlem2  27229  dchrisum0lem1b  27254  dchrisum0lem1  27255  pntrlog2bndlem6  27322  pntlemf  27344  precsexlem6  27897  precsexlem7  27898  sltonold  27926  nbupgruvtxres  28931  umgr2adedgwlk  29466  umgr2adedgwlkon  29467  umgr2adedgspth  29469  ex-res  29961  spanss2  30865  mdsymi  31931  padct  32211  cycpmco2lem5  32559  cycpmco2lem6  32560  cycpmco2lem7  32561  cycpmco2  32562  fldgenssid  32673  ordtconnlem1  33202  issgon  33419  sssigagen  33441  measiuns  33513  sitgclg  33639  cvmliftlem10  34583  satfsschain  34653  fmlasssuc  34678  satfun  34700  rdgssun  36562  ftc1anclem6  36869  heibor1lem  36980  heibor  36992  divrngcl  37128  isdrngo2  37129  igenss  37233  paddunssN  38982  sspadd1  38989  sspadd2  38990  pclssidN  39069  diassdvaN  40234  dochvalr  40531  lcdvbase  40767  nacsfix  41752  isnumbasgrplem2  42148  rgspnssid  42214  tfsconcatrnss12  42401  trrelsuperrel2dg  42724  fvilbd  42742  relexp0a  42769  wnefimgd  43215  grumnudlem  43346  icccncfext  44901  iblsplit  44980  dirkeritg  45116  dirkercncflem2  45118  fourierdlem81  45201  fourierdlem89  45209  fourierdlem91  45211  fourierdlem92  45212  fourierdlem111  45231  fouriercn  45246  hspdifhsp  45630  gsumsplit2f  46856  srhmsubc  47062  srhmsubcALTV  47080  fdivmpt  47313  fdivpm  47316  refdivpm  47317  mreclat  47709  elpglem2  47844