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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  unissint  4903  resdif  6737  fimacnvOLD  6948  tfrlem5  8211  domss2  8923  dffi3  9190  cantnfp1lem3  9438  trcl  9486  tcid  9497  r1ordg  9536  r1sssuc  9541  ackbij1lem15  9990  cfsmolem  10026  fin1a2lem7  10162  wunex2  10494  wuncid  10499  trclfvlb  14719  rtrclreclem2  14770  fsumsplit  15453  o1fsum  15525  fprodsplit  15676  phimullem  16480  vdwlem6  16687  ressinbas  16955  mrcssid  17326  mreexexlem2d  17354  acsfiindd  18271  dirge  18321  symgbasfi  18986  efgredlemf  19347  efgredlemd  19350  gsumzres  19510  gsumzcl2  19511  gsumzf1o  19513  gsumadd  19524  gsumzsplit  19528  gsumsplit2  19530  dprd2da  19645  dmdprdsplit2lem  19648  dmdprdsplit2  19649  dmdprdsplit  19650  dprdsplit  19651  invrpropd  19940  issubdrg  20049  lspssid  20247  pjcss  20923  aspssid  21082  istopon  22061  sscls  22207  ordtbas  22343  cncls2  22424  tgcmp  22552  cmpfi  22559  1stcfb  22596  1stckgenlem  22704  ptbasfi  22732  ptcnplem  22772  ptuncnv  22958  ptunhmeo  22959  fbasrn  23035  cnflf2  23154  fclscmp  23181  alexsublem  23195  ghmcnp  23266  tsmsgsum  23290  tsmsres  23295  tsmssplit  23303  tsmsxplem1  23304  ustssco  23366  mopnfss  23596  cnmpopc  24091  uniiccdif  24742  uniioombllem3  24749  uniioombllem4  24750  itg2splitlem  24913  itg2split  24914  itgsplit  25000  ellimc2  25041  ellimc3  25043  lhop  25180  itgpowd  25214  plyaddlem1  25374  plymullem1  25375  taylthlem2  25533  mtest  25563  xrlimcnp  26118  fsumharmonic  26161  chtdif  26307  dchrghm  26404  lgsquadlem2  26529  dchrisumlema  26636  dchrisumlem2  26638  dchrisum0lem1b  26663  dchrisum0lem1  26664  pntrlog2bndlem6  26731  pntlemf  26753  nbupgruvtxres  27774  umgr2adedgwlk  28310  umgr2adedgwlkon  28311  umgr2adedgspth  28313  ex-res  28805  spanss2  29707  mdsymi  30773  padct  31054  cycpmco2lem5  31397  cycpmco2lem6  31398  cycpmco2lem7  31399  cycpmco2  31400  ordtconnlem1  31874  issgon  32091  sssigagen  32113  measiuns  32185  sitgclg  32309  cvmliftlem10  33256  satfsschain  33326  fmlasssuc  33351  satfun  33373  rdgssun  35549  ftc1anclem6  35855  heibor1lem  35967  heibor  35979  divrngcl  36115  isdrngo2  36116  igenss  36220  paddunssN  37822  sspadd1  37829  sspadd2  37830  pclssidN  37909  diassdvaN  39074  dochvalr  39371  lcdvbase  39607  nacsfix  40534  isnumbasgrplem2  40929  rgspnssid  40995  trrelsuperrel2dg  41279  fvilbd  41297  relexp0a  41324  wnefimgd  41772  grumnudlem  41903  icccncfext  43428  iblsplit  43507  dirkeritg  43643  dirkercncflem2  43645  fourierdlem81  43728  fourierdlem89  43736  fourierdlem91  43738  fourierdlem92  43739  fourierdlem111  43758  fouriercn  43773  hspdifhsp  44154  gsumsplit2f  45374  srhmsubc  45634  srhmsubcALTV  45652  fdivmpt  45886  fdivpm  45889  refdivpm  45890  mreclat  46283  elpglem2  46417