Theorem sseqtrrid 3979

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  unissint  4929  resdif  6803  tfrlem5  8321  naddunif  8631  domss2  9076  dffi3  9346  cantnfp1lem3  9601  trcl  9649  tcid  9658  r1ordg  9702  r1sssuc  9707  ackbij1lem15  10155  cfsmolem  10192  fin1a2lem7  10328  wunex2  10661  wuncid  10666  trclfvlb  14943  rtrclreclem2  14994  fsumsplit  15676  o1fsum  15748  fprodsplit  15901  phimullem  16718  vdwlem6  16926  ressinbas  17184  mrcssid  17552  mreexexlem2d  17580  acsfiindd  18488  dirge  18538  symgbasfi  19320  efgredlemf  19682  efgredlemd  19685  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumadd  19864  gsumzsplit  19868  gsumsplit2  19870  dprd2da  19985  dmdprdsplit2lem  19988  dmdprdsplit2  19989  dmdprdsplit  19990  dprdsplit  19991  invrpropd  20366  rgspnssid  20559  srhmsubc  20625  issubdrg  20725  lspssid  20948  pjcss  21683  aspssid  21845  psdmul  22121  istopon  22868  sscls  23012  ordtbas  23148  cncls2  23229  tgcmp  23357  cmpfi  23364  1stcfb  23401  1stckgenlem  23509  ptbasfi  23537  ptcnplem  23577  ptuncnv  23763  ptunhmeo  23764  fbasrn  23840  cnflf2  23959  fclscmp  23986  alexsublem  24000  ghmcnp  24071  tsmsgsum  24095  tsmsres  24100  tsmssplit  24108  tsmsxplem1  24109  ustssco  24171  mopnfss  24399  cnmpopc  24890  uniiccdif  25547  uniioombllem3  25554  uniioombllem4  25555  itg2splitlem  25717  itg2split  25718  itgsplit  25805  ellimc2  25846  ellimc3  25848  lhop  25989  itgpowd  26025  plyaddlem1  26186  plymullem1  26187  taylthlem2  26350  taylthlem2OLD  26351  mtest  26381  xrlimcnp  26946  fsumharmonic  26990  chtdif  27136  dchrghm  27235  lgsquadlem2  27360  dchrisumlema  27467  dchrisumlem2  27469  dchrisum0lem1b  27494  dchrisum0lem1  27495  pntrlog2bndlem6  27562  pntlemf  27584  precsexlem6  28220  precsexlem7  28221  ltonold  28269  nbupgruvtxres  29492  cyclnumvtx  29885  umgr2adedgwlk  30030  umgr2adedgwlkon  30031  umgr2adedgspth  30033  ex-res  30528  spanss2  31432  mdsymi  32498  padct  32807  cycpmco2lem5  33223  cycpmco2lem6  33224  cycpmco2lem7  33225  cycpmco2  33226  fldgenssid  33406  vietalem  33755  ordtconnlem1  34101  issgon  34300  sssigagen  34322  measiuns  34394  sitgclg  34519  cvmliftlem10  35507  satfsschain  35577  fmlasssuc  35602  satfun  35624  rdgssun  37627  ftc1anclem6  37943  heibor1lem  38054  heibor  38066  divrngcl  38202  isdrngo2  38203  igenss  38307  paddunssN  40178  sspadd1  40185  sspadd2  40186  pclssidN  40265  diassdvaN  41430  dochvalr  41727  lcdvbase  41963  nacsfix  43063  isnumbasgrplem2  43455  tfsconcatrnss12  43700  trrelsuperrel2dg  44021  fvilbd  44039  relexp0a  44066  wnefimgd  44511  grumnudlem  44635  icccncfext  46239  iblsplit  46318  dirkeritg  46454  dirkercncflem2  46456  fourierdlem81  46539  fourierdlem89  46547  fourierdlem91  46549  fourierdlem92  46550  fourierdlem111  46569  fouriercn  46584  hspdifhsp  46968  3f1oss1  47429  dfnbgrss  48206  dfnbgrss2  48213  gsumsplit2f  48534  srhmsubcALTV  48679  fdivmpt  48894  fdivpm  48897  refdivpm  48898  mreclat  49350  elpglem2  50065