Theorem sseqtrrid 3974

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  unissint  4922  resdif  6789  tfrlem5  8305  naddunif  8614  domss2  9056  dffi3  9322  cantnfp1lem3  9577  trcl  9625  tcid  9634  r1ordg  9678  r1sssuc  9683  ackbij1lem15  10131  cfsmolem  10168  fin1a2lem7  10304  wunex2  10636  wuncid  10641  trclfvlb  14917  rtrclreclem2  14968  fsumsplit  15650  o1fsum  15722  fprodsplit  15875  phimullem  16692  vdwlem6  16900  ressinbas  17158  mrcssid  17525  mreexexlem2d  17553  acsfiindd  18461  dirge  18511  symgbasfi  19293  efgredlemf  19655  efgredlemd  19658  gsumzres  19823  gsumzcl2  19824  gsumzf1o  19826  gsumadd  19837  gsumzsplit  19841  gsumsplit2  19843  dprd2da  19958  dmdprdsplit2lem  19961  dmdprdsplit2  19962  dmdprdsplit  19963  dprdsplit  19964  invrpropd  20338  rgspnssid  20531  srhmsubc  20597  issubdrg  20697  lspssid  20920  pjcss  21655  aspssid  21817  psdmul  22082  istopon  22828  sscls  22972  ordtbas  23108  cncls2  23189  tgcmp  23317  cmpfi  23324  1stcfb  23361  1stckgenlem  23469  ptbasfi  23497  ptcnplem  23537  ptuncnv  23723  ptunhmeo  23724  fbasrn  23800  cnflf2  23919  fclscmp  23946  alexsublem  23960  ghmcnp  24031  tsmsgsum  24055  tsmsres  24060  tsmssplit  24068  tsmsxplem1  24069  ustssco  24131  mopnfss  24359  cnmpopc  24850  uniiccdif  25507  uniioombllem3  25514  uniioombllem4  25515  itg2splitlem  25677  itg2split  25678  itgsplit  25765  ellimc2  25806  ellimc3  25808  lhop  25949  itgpowd  25985  plyaddlem1  26146  plymullem1  26147  taylthlem2  26310  taylthlem2OLD  26311  mtest  26341  xrlimcnp  26906  fsumharmonic  26950  chtdif  27096  dchrghm  27195  lgsquadlem2  27320  dchrisumlema  27427  dchrisumlem2  27429  dchrisum0lem1b  27454  dchrisum0lem1  27455  pntrlog2bndlem6  27522  pntlemf  27544  precsexlem6  28151  precsexlem7  28152  sltonold  28199  nbupgruvtxres  29387  cyclnumvtx  29780  umgr2adedgwlk  29925  umgr2adedgwlkon  29926  umgr2adedgspth  29928  ex-res  30423  spanss2  31327  mdsymi  32393  padct  32705  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmco2  33109  fldgenssid  33286  ordtconnlem1  33958  issgon  34157  sssigagen  34179  measiuns  34251  sitgclg  34376  cvmliftlem10  35359  satfsschain  35429  fmlasssuc  35454  satfun  35476  rdgssun  37443  ftc1anclem6  37758  heibor1lem  37869  heibor  37881  divrngcl  38017  isdrngo2  38018  igenss  38122  paddunssN  39927  sspadd1  39934  sspadd2  39935  pclssidN  40014  diassdvaN  41179  dochvalr  41476  lcdvbase  41712  nacsfix  42829  isnumbasgrplem2  43221  tfsconcatrnss12  43466  trrelsuperrel2dg  43788  fvilbd  43806  relexp0a  43833  wnefimgd  44278  grumnudlem  44402  icccncfext  46009  iblsplit  46088  dirkeritg  46224  dirkercncflem2  46226  fourierdlem81  46309  fourierdlem89  46317  fourierdlem91  46319  fourierdlem92  46320  fourierdlem111  46339  fouriercn  46354  hspdifhsp  46738  3f1oss1  47199  dfnbgrss  47976  dfnbgrss2  47983  gsumsplit2f  48304  srhmsubcALTV  48449  fdivmpt  48665  fdivpm  48668  refdivpm  48669  mreclat  49121  elpglem2  49837