Theorem sseqtrrid 3993

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  unissint  4939  resdif  6824  tfrlem5  8351  naddunif  8660  domss2  9106  dffi3  9389  cantnfp1lem3  9640  trcl  9688  tcid  9699  r1ordg  9738  r1sssuc  9743  ackbij1lem15  10193  cfsmolem  10230  fin1a2lem7  10366  wunex2  10698  wuncid  10703  trclfvlb  14981  rtrclreclem2  15032  fsumsplit  15714  o1fsum  15786  fprodsplit  15939  phimullem  16756  vdwlem6  16964  ressinbas  17222  mrcssid  17585  mreexexlem2d  17613  acsfiindd  18519  dirge  18569  symgbasfi  19316  efgredlemf  19678  efgredlemd  19681  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumadd  19860  gsumzsplit  19864  gsumsplit2  19866  dprd2da  19981  dmdprdsplit2lem  19984  dmdprdsplit2  19985  dmdprdsplit  19986  dprdsplit  19987  invrpropd  20334  rgspnssid  20530  srhmsubc  20596  issubdrg  20696  lspssid  20898  pjcss  21632  aspssid  21794  psdmul  22060  istopon  22806  sscls  22950  ordtbas  23086  cncls2  23167  tgcmp  23295  cmpfi  23302  1stcfb  23339  1stckgenlem  23447  ptbasfi  23475  ptcnplem  23515  ptuncnv  23701  ptunhmeo  23702  fbasrn  23778  cnflf2  23897  fclscmp  23924  alexsublem  23938  ghmcnp  24009  tsmsgsum  24033  tsmsres  24038  tsmssplit  24046  tsmsxplem1  24047  ustssco  24109  mopnfss  24338  cnmpopc  24829  uniiccdif  25486  uniioombllem3  25493  uniioombllem4  25494  itg2splitlem  25656  itg2split  25657  itgsplit  25744  ellimc2  25785  ellimc3  25787  lhop  25928  itgpowd  25964  plyaddlem1  26125  plymullem1  26126  taylthlem2  26289  taylthlem2OLD  26290  mtest  26320  xrlimcnp  26885  fsumharmonic  26929  chtdif  27075  dchrghm  27174  lgsquadlem2  27299  dchrisumlema  27406  dchrisumlem2  27408  dchrisum0lem1b  27433  dchrisum0lem1  27434  pntrlog2bndlem6  27501  pntlemf  27523  precsexlem6  28121  precsexlem7  28122  sltonold  28169  nbupgruvtxres  29341  cyclnumvtx  29737  umgr2adedgwlk  29882  umgr2adedgwlkon  29883  umgr2adedgspth  29885  ex-res  30377  spanss2  31281  mdsymi  32347  padct  32650  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  fldgenssid  33270  ordtconnlem1  33921  issgon  34120  sssigagen  34142  measiuns  34214  sitgclg  34340  cvmliftlem10  35288  satfsschain  35358  fmlasssuc  35383  satfun  35405  rdgssun  37373  ftc1anclem6  37699  heibor1lem  37810  heibor  37822  divrngcl  37958  isdrngo2  37959  igenss  38063  paddunssN  39809  sspadd1  39816  sspadd2  39817  pclssidN  39896  diassdvaN  41061  dochvalr  41358  lcdvbase  41594  nacsfix  42707  isnumbasgrplem2  43100  tfsconcatrnss12  43345  trrelsuperrel2dg  43667  fvilbd  43685  relexp0a  43712  wnefimgd  44157  grumnudlem  44281  icccncfext  45892  iblsplit  45971  dirkeritg  46107  dirkercncflem2  46109  fourierdlem81  46192  fourierdlem89  46200  fourierdlem91  46202  fourierdlem92  46203  fourierdlem111  46222  fouriercn  46237  hspdifhsp  46621  3f1oss1  47080  dfnbgrss  47856  dfnbgrss2  47863  gsumsplit2f  48172  srhmsubcALTV  48317  fdivmpt  48533  fdivpm  48536  refdivpm  48537  mreclat  48989  elpglem2  49705