Theorem sseqtrid 3980

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseqtrrid  3981  iunxdif3  5062  fssdm  6727  fndmdif  7039  fneqeql2  7044  fconst4  7214  isofrlem  7340  fvmptopab  7467  f1opw2  7667  fparlem3  8110  fparlem4  8111  fnwelem  8128  fsuppeq  8172  fsuppeqg  8173  ecss  8747  pw2f1olem  9070  fopwdom  9074  ssenen  9140  ssfiALT  9159  fiint  9287  f1opwfi  9314  kmlem5  10139  enfin2i  10306  fpwwe2lem5  10621  fpwwe2lem8  10624  tskuni  10769  monoord2  14071  seqz  14088  cshimadifsn0  14869  binom1dif  15889  bpolycl  16107  bpolysum  16108  bpolydiflem  16109  bitsres  16532  prdshom  17521  imasless  17595  cntzval  19392  f1omvdmvd  19514  f1omvdconj  19517  pmtrfb  19536  symggen  19541  symggen2  19542  psgnunilem1  19564  gsumzaddlem  19992  rngcbas  20707  ringcbas  20736  isdrngd  20850  isdrngdOLD  20852  lspextmo  21158  znleval  21685  freshmansdream  21705  ordtcld1  23335  ordtcld2  23336  cnpnei  23402  cnntri  23409  cncls2  23411  cncls  23412  cnntr  23413  cncnp  23418  cndis  23429  paste  23432  cmpfi  23546  conncompcld  23572  1stcfb  23583  1stccnp  23600  cldllycmp  23633  llycmpkgen2  23688  kgencn  23694  kgencn3  23696  dfac14lem  23755  txdis1cn  23773  hausdiag  23783  txkgen  23790  qtopval2  23834  basqtop  23849  qtopcld  23851  qtopeu  23854  qtoprest  23855  imastopn  23858  hmeontr  23907  hmeoimaf1o  23908  cmphaushmeo  23938  ordthmeolem  23939  elfm3  24088  rnelfmlem  24090  rnelfm  24091  alexsubALTlem4  24188  cldsubg  24249  tgpconncompeqg  24250  tgpconncomp  24251  qustgpopn  24258  qustgplem  24259  tsmsf1o  24283  ucncn  24422  imasf1oxms  24627  blcld  24643  metustfbas  24695  cfilucfil  24697  metuel2  24703  icchmeo  25081  relcmpcmet  25458  minveclem4a  25570  nulmbl2  25676  icombl  25704  ioombl  25705  uniiccdif  25718  volivth  25747  mbfres2  25785  itg1addlem5  25840  itgsplitioo  25978  dvcobr  26086  dvcnvlem  26116  lhop1lem  26153  lhop  26156  dvcnvrelem2  26158  uc1pval  26278  mon1pval  26280  vieta1lem2  26453  basellem5  27230  onnolt  28440  f1otrg  29201  axlowdimlem13  29285  axcontlem10  29304  uhgrspansubgr  29622  vtxdun  29812  pthdlem1  30096  eucrct2eupth  30577  ssmd1  32644  mdslj2i  32653  atcvat4i  32730  imadifxp  32927  nfpconfp  32958  2ndresdju  32975  ofpreima  32991  ofpreima2  32992  fsuppcurry1  33050  fsuppcurry2  33051  indpreima  33166  indf1ofs  33167  ccatws1f1olast  33253  gsumpart  33364  symgcom  33384  symgcom2  33385  pmtrcnel  33390  cycpmfvlem  33413  cycpmfv3  33416  elrgspnsubrunlem2  33549  elrspunidl  33717  idlinsubrg  33720  esplymhp  33939  esplyfval1  33944  esplyfvaln  33945  fldextrspunlsp  34045  qtophaus  34207  reff  34210  locfinreflem  34211  zarcmplem  34252  hauseqcn  34269  oms0  34668  eulerpartlemv  34735  eulerpartlemb  34739  eulerpartlemr  34745  eulerpartlemgs2  34751  eulerpartlemn  34752  ballotlemro  34894  bnj1253  35386  bnj1280  35389  onvfowev  35581  pthhashvtx  35601  acycgr0v  35621  prclisacycgr  35624  subfacp1lem3  35655  cvmscld  35746  cvmsss2  35747  cvmliftmolem1  35754  cvmliftlem7  35764  cvmlift2lem9  35784  cvmlift3lem7  35798  fnessref  36849  tailf  36867  poimirlem3  38255  mbfresfi  38298  cnambfre  38300  itg2addnclem2  38304  mettrifi  38389  ismtyres  38440  isdrngo2  38590  press  39129  diaintclN  41813  dibintclN  41922  dihintcl  42099  dochocss  42121  mapdunirnN  42405  pw2f1ocnv  43747  wessf1ornlem  45886  monoord2xrv  46180  itgcoscmulx  46666  ibliooicc  46668  stoweidlem11  46708  stoweidlem34  46731  fourierdlem48  46851  fourierdlem49  46852  fourierdlem74  46877  uniimaprimaeqfv  48114  elsetpreimafvssdm  48118  fdivmptf  49304  refdivmptf  49305  iscnrm3llem2  49711  imaidfu  49871