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  6805  tfrlem5  8323  naddunif  8633  domss2  9078  dffi3  9348  cantnfp1lem3  9603  trcl  9651  tcid  9660  r1ordg  9704  r1sssuc  9709  ackbij1lem15  10157  cfsmolem  10194  fin1a2lem7  10330  wunex2  10663  wuncid  10668  trclfvlb  14945  rtrclreclem2  14996  fsumsplit  15678  o1fsum  15750  fprodsplit  15903  phimullem  16720  vdwlem6  16928  ressinbas  17186  mrcssid  17554  mreexexlem2d  17582  acsfiindd  18490  dirge  18540  symgbasfi  19325  efgredlemf  19687  efgredlemd  19690  gsumzres  19855  gsumzcl2  19856  gsumzf1o  19858  gsumadd  19869  gsumzsplit  19873  gsumsplit2  19875  dprd2da  19990  dmdprdsplit2lem  19993  dmdprdsplit2  19994  dmdprdsplit  19995  dprdsplit  19996  invrpropd  20371  rgspnssid  20564  srhmsubc  20630  issubdrg  20730  lspssid  20953  pjcss  21688  aspssid  21850  psdmul  22126  istopon  22873  sscls  23017  ordtbas  23153  cncls2  23234  tgcmp  23362  cmpfi  23369  1stcfb  23406  1stckgenlem  23514  ptbasfi  23542  ptcnplem  23582  ptuncnv  23768  ptunhmeo  23769  fbasrn  23845  cnflf2  23964  fclscmp  23991  alexsublem  24005  ghmcnp  24076  tsmsgsum  24100  tsmsres  24105  tsmssplit  24113  tsmsxplem1  24114  ustssco  24176  mopnfss  24404  cnmpopc  24895  uniiccdif  25552  uniioombllem3  25559  uniioombllem4  25560  itg2splitlem  25722  itg2split  25723  itgsplit  25810  ellimc2  25851  ellimc3  25853  lhop  25994  itgpowd  26030  plyaddlem1  26191  plymullem1  26192  taylthlem2  26355  taylthlem2OLD  26356  mtest  26386  xrlimcnp  26951  fsumharmonic  26995  chtdif  27141  dchrghm  27240  lgsquadlem2  27365  dchrisumlema  27472  dchrisumlem2  27474  dchrisum0lem1b  27499  dchrisum0lem1  27500  pntrlog2bndlem6  27567  pntlemf  27589  precsexlem6  28225  precsexlem7  28226  ltonold  28274  nbupgruvtxres  29498  cyclnumvtx  29891  umgr2adedgwlk  30036  umgr2adedgwlkon  30037  umgr2adedgspth  30039  ex-res  30534  spanss2  31439  mdsymi  32505  cycpmco2lem5  33230  cycpmco2lem6  33231  cycpmco2lem7  33232  cycpmco2  33233  fldgenssid  33413  vietalem  33762  ordtconnlem1  34108  issgon  34307  sssigagen  34329  measiuns  34401  sitgclg  34526  cvmliftlem10  35516  satfsschain  35586  fmlasssuc  35611  satfun  35633  rdgssun  37660  ftc1anclem6  37978  heibor1lem  38089  heibor  38101  divrngcl  38237  isdrngo2  38238  igenss  38342  paddunssN  40213  sspadd1  40220  sspadd2  40221  pclssidN  40300  diassdvaN  41465  dochvalr  41762  lcdvbase  41998  nacsfix  43098  isnumbasgrplem2  43490  tfsconcatrnss12  43735  trrelsuperrel2dg  44056  fvilbd  44074  relexp0a  44101  wnefimgd  44546  grumnudlem  44670  icccncfext  46274  iblsplit  46353  dirkeritg  46489  dirkercncflem2  46491  fourierdlem81  46574  fourierdlem89  46582  fourierdlem91  46584  fourierdlem92  46585  fourierdlem111  46604  fouriercn  46619  hspdifhsp  47003  3f1oss1  47464  dfnbgrss  48241  dfnbgrss2  48248  gsumsplit2f  48569  srhmsubcALTV  48714  fdivmpt  48929  fdivpm  48932  refdivpm  48933  mreclat  49385  elpglem2  50100