Theorem sseqtrrid 3981

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  unissint  4938  resdif  6844  tfrlem5  8367  naddunif  8681  domss2  9125  dffi3  9392  cantnfp1lem3  9650  trcl  9698  tcid  9707  r1ordg  9751  r1sssuc  9756  ackbij1lem15  10217  cfsmolem  10255  fin1a2lem7  10391  wunex2  10724  wuncid  10729  trclfvlb  15047  rtrclreclem2  15098  fsumsplit  15794  o1fsum  15867  fprodsplit  16022  phimullem  16839  vdwlem6  17047  ressinbas  17306  mrcssid  17674  mreexexlem2d  17702  acsfiindd  18610  dirge  18660  symgbasfi  19450  efgredlemf  19812  efgredlemd  19815  gsumzres  19980  gsumzcl2  19981  gsumzf1o  19983  gsumadd  19994  gsumzsplit  19998  gsumsplit2  20000  dprd2da  20115  dmdprdsplit2lem  20118  dmdprdsplit2  20119  dmdprdsplit  20120  dprdsplit  20121  invrpropd  20501  rgspnssid  20700  srhmsubc  20766  issubdrg  20864  lspssid  21087  pjcss  21847  aspssid  22008  psdmul  22310  istopon  23050  sscls  23194  ordtbas  23330  cncls2  23411  tgcmp  23539  cmpfi  23546  1stcfb  23583  1stckgenlem  23691  ptbasfi  23719  ptcnplem  23759  ptuncnv  23945  ptunhmeo  23946  fbasrn  24022  cnflf2  24141  fclscmp  24168  alexsublem  24182  ghmcnp  24253  tsmsgsum  24277  tsmsres  24282  tsmssplit  24290  tsmsxplem1  24291  ustssco  24353  mopnfss  24581  cnmpopc  25068  uniiccdif  25718  uniioombllem3  25725  uniioombllem4  25726  itg2splitlem  25888  itg2split  25889  itgsplit  25976  ellimc2  26017  ellimc3  26019  lhop  26156  itgpowd  26190  plyaddlem1  26351  plymullem1  26352  taylthlem2  26515  mtest  26545  xrlimcnp  27111  fsumharmonic  27154  chtdif  27300  dchrghm  27398  lgsquadlem2  27523  dchrisumlema  27630  dchrisumlem2  27632  dchrisum0lem1b  27657  dchrisum0lem1  27658  pntrlog2bndlem6  27725  pntlemf  27747  precsexlem6  28383  precsexlem7  28384  ltonold  28432  nbupgruvtxres  29735  cyclnumvtx  30127  umgr2adedgwlk  30272  umgr2adedgwlkon  30273  umgr2adedgspth  30275  ex-res  30770  spanss2  31675  mdsymi  32741  cycpmco2lem5  33428  cycpmco2lem6  33429  cycpmco2lem7  33430  cycpmco2  33431  fldgenssid  33612  vietalem  33947  ordtconnlem1  34292  issgon  34491  sssigagen  34513  measiuns  34585  sitgclg  34710  cvmliftlem10  35764  satfsschain  35834  fmlasssuc  35859  satfun  35881  dfttc3gw  37012  rdgssun  38002  ftc1anclem6  38327  heibor1lem  38438  heibor  38450  divrngcl  38586  isdrngo2  38587  igenss  38691  paddunssN  40560  sspadd1  40567  sspadd2  40568  pclssidN  40647  diassdvaN  41812  dochvalr  42109  lcdvbase  42345  nacsfix  43423  isnumbasgrplem2  43811  tfsconcatrnss12  44056  trrelsuperrel2dg  44377  fvilbd  44395  relexp0a  44422  wnefimgd  44867  grumnudlem  44975  icccncfext  46581  iblsplit  46660  dirkeritg  46796  dirkercncflem2  46798  fourierdlem81  46881  fourierdlem89  46889  fourierdlem91  46891  fourierdlem92  46892  fourierdlem111  46911  fouriercn  46926  hspdifhsp  47310  3f1oss1  47789  dfnbgrss  48594  dfnbgrss2  48601  gsumsplit2f  48922  srhmsubcALTV  49067  fdivmpt  49297  fdivpm  49300  refdivpm  49301  mreclat  49752  elpglem2  50467