Theorem sseqtrrid 3968

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 3956	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  unissint  4862  resdif  6610  fimacnv  6816  tfrlem5  7999  domss2  8660  dffi3  8879  cantnfp1lem3  9127  trcl  9154  tcid  9165  r1ordg  9191  r1sssuc  9196  ackbij1lem15  9645  cfsmolem  9681  fin1a2lem7  9817  wunex2  10149  wuncid  10154  trclfvlb  14359  rtrclreclem2  14410  fsumsplit  15089  o1fsum  15160  fprodsplit  15312  phimullem  16106  vdwlem6  16312  ressinbas  16552  mrcssid  16880  mreexexlem2d  16908  acsfiindd  17779  dirge  17839  symgbasfi  18499  efgredlemf  18859  efgredlemd  18862  gsumzres  19022  gsumzcl2  19023  gsumzf1o  19025  gsumadd  19036  gsumzsplit  19040  gsumsplit2  19042  dprd2da  19157  dmdprdsplit2lem  19160  dmdprdsplit2  19161  dmdprdsplit  19162  dprdsplit  19163  invrpropd  19444  issubdrg  19553  lspssid  19750  pjcss  20405  aspssid  20564  istopon  21517  sscls  21661  ordtbas  21797  cncls2  21878  tgcmp  22006  cmpfi  22013  1stcfb  22050  1stckgenlem  22158  ptbasfi  22186  ptcnplem  22226  ptuncnv  22412  ptunhmeo  22413  fbasrn  22489  cnflf2  22608  fclscmp  22635  alexsublem  22649  ghmcnp  22720  tsmsgsum  22744  tsmsres  22749  tsmssplit  22757  tsmsxplem1  22758  ustssco  22820  mopnfss  23050  cnmpopc  23533  uniiccdif  24182  uniioombllem3  24189  uniioombllem4  24190  itg2splitlem  24352  itg2split  24353  itgsplit  24439  ellimc2  24480  ellimc3  24482  lhop  24619  itgpowd  24653  plyaddlem1  24810  plymullem1  24811  taylthlem2  24969  mtest  24999  xrlimcnp  25554  fsumharmonic  25597  chtdif  25743  dchrghm  25840  lgsquadlem2  25965  dchrisumlema  26072  dchrisumlem2  26074  dchrisum0lem1b  26099  dchrisum0lem1  26100  pntrlog2bndlem6  26167  pntlemf  26189  nbupgruvtxres  27197  umgr2adedgwlk  27731  umgr2adedgwlkon  27732  umgr2adedgspth  27734  ex-res  28226  spanss2  29128  mdsymi  30194  padct  30481  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  ordtconnlem1  31277  issgon  31492  sssigagen  31514  measiuns  31586  sitgclg  31710  cvmliftlem10  32654  satfsschain  32724  fmlasssuc  32749  satfun  32771  rdgssun  34795  ftc1anclem6  35135  heibor1lem  35247  heibor  35259  divrngcl  35395  isdrngo2  35396  igenss  35500  paddunssN  37104  sspadd1  37111  sspadd2  37112  pclssidN  37191  diassdvaN  38356  dochvalr  38653  lcdvbase  38889  nacsfix  39653  isnumbasgrplem2  40048  rgspnssid  40114  trrelsuperrel2dg  40372  fvilbd  40390  relexp0a  40417  wnefimgd  40865  grumnudlem  40993  icccncfext  42529  iblsplit  42608  dirkeritg  42744  dirkercncflem2  42746  fourierdlem81  42829  fourierdlem89  42837  fourierdlem91  42839  fourierdlem92  42840  fourierdlem111  42859  fouriercn  42874  hspdifhsp  43255  gsumsplit2f  44440  srhmsubc  44700  srhmsubcALTV  44718  fdivmpt  44954  fdivpm  44957  refdivpm  44958  elpglem2  45241