Theorem sseqtrid 3964

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sseqtrid.1	⊢ 𝐵 ⊆ 𝐴
sseqtrid.2	⊢ (𝜑 → 𝐴 = 𝐶)

Assertion

Ref	Expression
sseqtrid	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem sseqtrid

Step	Hyp	Ref	Expression
1		sseqtrid.1	. . 3 ⊢ 𝐵 ⊆ 𝐴
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		sseqtrid.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	sseqtrd 3958	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseqtrrid  3965  iunxdif3  5031  fssdm  6681  fndmdif  6990  fneqeql2  6995  fconst4  7165  isofrlem  7291  fvmptopab  7418  f1opw2  7618  fparlem3  8060  fparlem4  8061  fnwelem  8078  fsuppeq  8122  fsuppeqg  8123  ecss  8692  pw2f1olem  9016  fopwdom  9020  ssenen  9086  ssfiALT  9105  fiint  9234  f1opwfi  9263  kmlem5  10075  enfin2i  10241  fpwwe2lem5  10556  fpwwe2lem8  10559  tskuni  10704  monoord2  13993  seqz  14010  cshimadifsn0  14790  binom1dif  15796  bpolycl  16015  bpolysum  16016  bpolydiflem  16017  bitsres  16440  prdshom  17428  imasless  17502  cntzval  19294  f1omvdmvd  19416  f1omvdconj  19419  pmtrfb  19438  symggen  19443  symggen2  19444  psgnunilem1  19466  gsumzaddlem  19894  rngcbas  20600  ringcbas  20629  isdrngd  20744  isdrngdOLD  20746  lspextmo  21053  znleval  21536  freshmansdream  21556  ordtcld1  23187  ordtcld2  23188  cnpnei  23254  cnntri  23261  cncls2  23263  cncls  23264  cnntr  23265  cncnp  23270  cndis  23281  paste  23284  cmpfi  23398  conncompcld  23424  1stcfb  23435  1stccnp  23452  cldllycmp  23485  llycmpkgen2  23540  kgencn  23546  kgencn3  23548  dfac14lem  23607  txdis1cn  23625  hausdiag  23635  txkgen  23642  qtopval2  23686  basqtop  23701  qtopcld  23703  qtopeu  23706  qtoprest  23707  imastopn  23710  hmeontr  23759  hmeoimaf1o  23760  cmphaushmeo  23790  ordthmeolem  23791  elfm3  23940  rnelfmlem  23942  rnelfm  23943  alexsubALTlem4  24040  cldsubg  24101  tgpconncompeqg  24102  tgpconncomp  24103  qustgpopn  24110  qustgplem  24111  tsmsf1o  24135  ucncn  24274  imasf1oxms  24479  blcld  24495  metustfbas  24547  cfilucfil  24549  metuel2  24555  icchmeo  24933  relcmpcmet  25310  minveclem4a  25422  nulmbl2  25528  icombl  25556  ioombl  25557  uniiccdif  25570  volivth  25599  mbfres2  25637  itg1addlem5  25692  itgsplitioo  25830  dvcobr  25938  dvcnvlem  25968  lhop1lem  26005  lhop  26008  dvcnvrelem2  26010  uc1pval  26130  mon1pval  26132  vieta1lem2  26302  basellem5  27073  onnolt  28283  f1otrg  28964  axlowdimlem13  29048  axcontlem10  29067  uhgrspansubgr  29385  vtxdun  29575  pthdlem1  29859  eucrct2eupth  30340  ssmd1  32407  mdslj2i  32416  atcvat4i  32493  imadifxp  32697  nfpconfp  32731  2ndresdju  32748  ofpreima  32764  ofpreima2  32765  fsuppcurry1  32823  fsuppcurry2  32824  indpreima  32951  indf1ofs  32952  ccatws1f1olast  33038  gsumpart  33151  symgcom  33171  symgcom2  33172  pmtrcnel  33177  cycpmfvlem  33200  cycpmfv3  33203  elrgspnsubrunlem2  33336  elrspunidl  33518  idlinsubrg  33521  esplymhp  33759  esplyfval1  33764  esplyfvaln  33765  fldextrspunlsp  33865  qtophaus  34027  reff  34030  locfinreflem  34031  zarcmplem  34072  hauseqcn  34089  oms0  34488  eulerpartlemv  34555  eulerpartlemb  34559  eulerpartlemr  34565  eulerpartlemgs2  34571  eulerpartlemn  34572  ballotlemro  34714  bnj1253  35206  bnj1280  35209  pthhashvtx  35363  acycgr0v  35383  prclisacycgr  35386  subfacp1lem3  35417  cvmscld  35508  cvmsss2  35509  cvmliftmolem1  35516  cvmliftlem7  35526  cvmlift2lem9  35546  cvmlift3lem7  35560  fnessref  36592  tailf  36610  poimirlem3  37997  mbfresfi  38040  cnambfre  38042  itg2addnclem2  38046  mettrifi  38131  ismtyres  38182  isdrngo2  38332  press  38873  diaintclN  41557  dibintclN  41666  dihintcl  41843  dochocss  41865  mapdunirnN  42149  pw2f1ocnv  43489  wessf1ornlem  45639  monoord2xrv  45933  itgcoscmulx  46419  ibliooicc  46421  stoweidlem11  46461  stoweidlem34  46484  fourierdlem48  46604  fourierdlem49  46605  fourierdlem74  46630  uniimaprimaeqfv  47864  elsetpreimafvssdm  47868  fdivmptf  49039  refdivmptf  49040  iscnrm3llem2  49447  imaidfu  49607