Theorem sseqtrrid 3946

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	. . 3 ⊢ 𝐵 ⊆ 𝐴
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		sseqtrrid.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
4	2, 3	sseqtrrd 3934	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3866  df-ss 3876

This theorem is referenced by:  unissint  4863  resdif  6623  fimacnv  6831  tfrlem5  8027  domss2  8698  dffi3  8921  cantnfp1lem3  9169  trcl  9196  tcid  9207  r1ordg  9233  r1sssuc  9238  ackbij1lem15  9687  cfsmolem  9723  fin1a2lem7  9859  wunex2  10191  wuncid  10196  trclfvlb  14408  rtrclreclem2  14459  fsumsplit  15138  o1fsum  15209  fprodsplit  15361  phimullem  16164  vdwlem6  16370  ressinbas  16611  mrcssid  16939  mreexexlem2d  16967  acsfiindd  17846  dirge  17906  symgbasfi  18567  efgredlemf  18927  efgredlemd  18930  gsumzres  19090  gsumzcl2  19091  gsumzf1o  19093  gsumadd  19104  gsumzsplit  19108  gsumsplit2  19110  dprd2da  19225  dmdprdsplit2lem  19228  dmdprdsplit2  19229  dmdprdsplit  19230  dprdsplit  19231  invrpropd  19512  issubdrg  19621  lspssid  19818  pjcss  20474  aspssid  20633  istopon  21605  sscls  21749  ordtbas  21885  cncls2  21966  tgcmp  22094  cmpfi  22101  1stcfb  22138  1stckgenlem  22246  ptbasfi  22274  ptcnplem  22314  ptuncnv  22500  ptunhmeo  22501  fbasrn  22577  cnflf2  22696  fclscmp  22723  alexsublem  22737  ghmcnp  22808  tsmsgsum  22832  tsmsres  22837  tsmssplit  22845  tsmsxplem1  22846  ustssco  22908  mopnfss  23138  cnmpopc  23622  uniiccdif  24271  uniioombllem3  24278  uniioombllem4  24279  itg2splitlem  24441  itg2split  24442  itgsplit  24528  ellimc2  24569  ellimc3  24571  lhop  24708  itgpowd  24742  plyaddlem1  24902  plymullem1  24903  taylthlem2  25061  mtest  25091  xrlimcnp  25646  fsumharmonic  25689  chtdif  25835  dchrghm  25932  lgsquadlem2  26057  dchrisumlema  26164  dchrisumlem2  26166  dchrisum0lem1b  26191  dchrisum0lem1  26192  pntrlog2bndlem6  26259  pntlemf  26281  nbupgruvtxres  27289  umgr2adedgwlk  27823  umgr2adedgwlkon  27824  umgr2adedgspth  27826  ex-res  28318  spanss2  29220  mdsymi  30286  padct  30571  cycpmco2lem5  30916  cycpmco2lem6  30917  cycpmco2lem7  30918  cycpmco2  30919  ordtconnlem1  31388  issgon  31603  sssigagen  31625  measiuns  31697  sitgclg  31821  cvmliftlem10  32765  satfsschain  32835  fmlasssuc  32860  satfun  32882  rdgssun  35068  ftc1anclem6  35408  heibor1lem  35520  heibor  35532  divrngcl  35668  isdrngo2  35669  igenss  35773  paddunssN  37377  sspadd1  37384  sspadd2  37385  pclssidN  37464  diassdvaN  38629  dochvalr  38926  lcdvbase  39162  nacsfix  40019  isnumbasgrplem2  40414  rgspnssid  40480  trrelsuperrel2dg  40738  fvilbd  40756  relexp0a  40783  wnefimgd  41231  grumnudlem  41359  icccncfext  42888  iblsplit  42967  dirkeritg  43103  dirkercncflem2  43105  fourierdlem81  43188  fourierdlem89  43196  fourierdlem91  43198  fourierdlem92  43199  fourierdlem111  43218  fouriercn  43233  hspdifhsp  43614  gsumsplit2f  44800  srhmsubc  45060  srhmsubcALTV  45078  fdivmpt  45312  fdivpm  45315  refdivpm  45316  elpglem2  45625