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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  unissint  4975  resdif  6851  fimacnvOLD  7069  tfrlem5  8376  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  14951  rtrclreclem2  15002  fsumsplit  15683  o1fsum  15755  fprodsplit  15906  phimullem  16708  vdwlem6  16915  ressinbas  17186  mrcssid  17557  mreexexlem2d  17585  acsfiindd  18502  dirge  18552  symgbasfi  19240  efgredlemf  19603  efgredlemd  19606  gsumzres  19771  gsumzcl2  19772  gsumzf1o  19774  gsumadd  19785  gsumzsplit  19789  gsumsplit2  19791  dprd2da  19906  dmdprdsplit2lem  19909  dmdprdsplit2  19910  dmdprdsplit  19911  dprdsplit  19912  invrpropd  20224  issubdrg  20381  lspssid  20588  pjcss  21262  aspssid  21423  istopon  22405  sscls  22551  ordtbas  22687  cncls2  22768  tgcmp  22896  cmpfi  22903  1stcfb  22940  1stckgenlem  23048  ptbasfi  23076  ptcnplem  23116  ptuncnv  23302  ptunhmeo  23303  fbasrn  23379  cnflf2  23498  fclscmp  23525  alexsublem  23539  ghmcnp  23610  tsmsgsum  23634  tsmsres  23639  tsmssplit  23647  tsmsxplem1  23648  ustssco  23710  mopnfss  23940  cnmpopc  24435  uniiccdif  25086  uniioombllem3  25093  uniioombllem4  25094  itg2splitlem  25257  itg2split  25258  itgsplit  25344  ellimc2  25385  ellimc3  25387  lhop  25524  itgpowd  25558  plyaddlem1  25718  plymullem1  25719  taylthlem2  25877  mtest  25907  xrlimcnp  26462  fsumharmonic  26505  chtdif  26651  dchrghm  26748  lgsquadlem2  26873  dchrisumlema  26980  dchrisumlem2  26982  dchrisum0lem1b  27007  dchrisum0lem1  27008  pntrlog2bndlem6  27075  pntlemf  27097  precsexlem6  27647  precsexlem7  27648  nbupgruvtxres  28653  umgr2adedgwlk  29188  umgr2adedgwlkon  29189  umgr2adedgspth  29191  ex-res  29683  spanss2  30585  mdsymi  31651  padct  31931  cycpmco2lem5  32276  cycpmco2lem6  32277  cycpmco2lem7  32278  cycpmco2  32279  fldgenssid  32391  ordtconnlem1  32892  issgon  33109  sssigagen  33131  measiuns  33203  sitgclg  33329  cvmliftlem10  34273  satfsschain  34343  fmlasssuc  34368  satfun  34390  rdgssun  36247  ftc1anclem6  36554  heibor1lem  36665  heibor  36677  divrngcl  36813  isdrngo2  36814  igenss  36918  paddunssN  38667  sspadd1  38674  sspadd2  38675  pclssidN  38754  diassdvaN  39919  dochvalr  40216  lcdvbase  40452  nacsfix  41435  isnumbasgrplem2  41831  rgspnssid  41897  tfsconcatrnss12  42084  trrelsuperrel2dg  42407  fvilbd  42425  relexp0a  42452  wnefimgd  42898  grumnudlem  43029  icccncfext  44589  iblsplit  44668  dirkeritg  44804  dirkercncflem2  44806  fourierdlem81  44889  fourierdlem89  44897  fourierdlem91  44899  fourierdlem92  44900  fourierdlem111  44919  fouriercn  44934  hspdifhsp  45318  gsumsplit2f  46576  srhmsubc  46927  srhmsubcALTV  46945  fdivmpt  47179  fdivpm  47182  refdivpm  47183  mreclat  47575  elpglem2  47710