Theorem sseqtrrid 4020

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  unissint  4900  resdif  6635  fimacnv  6839  tfrlem5  8016  domss2  8676  dffi3  8895  cantnfp1lem3  9143  trcl  9170  tcid  9181  r1ordg  9207  r1sssuc  9212  ackbij1lem15  9656  cfsmolem  9692  fin1a2lem7  9828  wunex2  10160  wuncid  10165  trclfvlb  14368  rtrclreclem1  14417  fsumsplit  15097  o1fsum  15168  fprodsplit  15320  phimullem  16116  vdwlem6  16322  ressinbas  16560  mrcssid  16888  mreexexlem2d  16916  acsfiindd  17787  dirge  17847  symgbasfi  18507  efgredlemf  18867  efgredlemd  18870  gsumzres  19029  gsumzcl2  19030  gsumzf1o  19032  gsumadd  19043  gsumzsplit  19047  gsumsplit2  19049  dprd2da  19164  dmdprdsplit2lem  19167  dmdprdsplit2  19168  dmdprdsplit  19169  dprdsplit  19170  invrpropd  19448  issubdrg  19560  lspssid  19757  aspssid  20107  pjcss  20860  istopon  21520  sscls  21664  ordtbas  21800  cncls2  21881  tgcmp  22009  cmpfi  22016  1stcfb  22053  1stckgenlem  22161  ptbasfi  22189  ptcnplem  22229  ptuncnv  22415  ptunhmeo  22416  fbasrn  22492  cnflf2  22611  fclscmp  22638  alexsublem  22652  ghmcnp  22723  tsmsgsum  22747  tsmsres  22752  tsmssplit  22760  tsmsxplem1  22761  ustssco  22823  mopnfss  23053  cnmpopc  23532  uniiccdif  24179  uniioombllem3  24186  uniioombllem4  24187  itg2splitlem  24349  itg2split  24350  itgsplit  24436  ellimc2  24475  ellimc3  24477  lhop  24613  plyaddlem1  24803  plymullem1  24804  taylthlem2  24962  mtest  24992  xrlimcnp  25546  fsumharmonic  25589  chtdif  25735  dchrghm  25832  lgsquadlem2  25957  dchrisumlema  26064  dchrisumlem2  26066  dchrisum0lem1b  26091  dchrisum0lem1  26092  pntrlog2bndlem6  26159  pntlemf  26181  nbupgruvtxres  27189  umgr2adedgwlk  27724  umgr2adedgwlkon  27725  umgr2adedgspth  27727  ex-res  28220  spanss2  29122  mdsymi  30188  padct  30455  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  ordtconnlem1  31167  issgon  31382  sssigagen  31404  measiuns  31476  sitgclg  31600  cvmliftlem10  32541  satfsschain  32611  fmlasssuc  32636  satfun  32658  rdgssun  34662  ftc1anclem6  34987  heibor1lem  35102  heibor  35114  divrngcl  35250  isdrngo2  35251  igenss  35355  paddunssN  36959  sspadd1  36966  sspadd2  36967  pclssidN  37046  diassdvaN  38211  dochvalr  38508  lcdvbase  38744  nacsfix  39358  isnumbasgrplem2  39753  rgspnssid  39819  itgpowd  39870  trrelsuperrel2dg  40065  fvilbd  40083  relexp0a  40110  wnefimgd  40561  grumnudlem  40670  icccncfext  42219  iblsplit  42300  dirkeritg  42436  dirkercncflem2  42438  fourierdlem81  42521  fourierdlem89  42529  fourierdlem91  42531  fourierdlem92  42532  fourierdlem111  42551  fouriercn  42566  hspdifhsp  42947  gsumsplit2f  44136  srhmsubc  44396  srhmsubcALTV  44414  fdivmpt  44649  fdivpm  44652  refdivpm  44653  elpglem2  44863