Theorem sseqtrid 3987

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  sseqtrrid  3988  iunxdif3  5062  fssdm  6723  fndmdif  7035  fneqeql2  7040  fconst4  7210  isofrlem  7336  fvmptopab  7463  f1opw2  7663  fparlem3  8105  fparlem4  8106  fnwelem  8123  fsuppeq  8167  fsuppeqg  8168  ecss  8742  pw2f1olem  9065  fopwdom  9069  ssenen  9135  ssfiALT  9154  fiint  9282  f1opwfi  9309  kmlem5  10134  enfin2i  10301  fpwwe2lem5  10616  fpwwe2lem8  10619  tskuni  10764  monoord2  14065  seqz  14082  cshimadifsn0  14863  binom1dif  15883  bpolycl  16102  bpolysum  16103  bpolydiflem  16104  bitsres  16527  prdshom  17516  imasless  17590  cntzval  19387  f1omvdmvd  19509  f1omvdconj  19512  pmtrfb  19531  symggen  19536  symggen2  19537  psgnunilem1  19559  gsumzaddlem  19987  rngcbas  20702  ringcbas  20731  isdrngd  20843  isdrngdOLD  20845  lspextmo  21151  znleval  21669  freshmansdream  21689  ordtcld1  23319  ordtcld2  23320  cnpnei  23386  cnntri  23393  cncls2  23395  cncls  23396  cnntr  23397  cncnp  23402  cndis  23413  paste  23416  cmpfi  23530  conncompcld  23556  1stcfb  23567  1stccnp  23584  cldllycmp  23617  llycmpkgen2  23672  kgencn  23678  kgencn3  23680  dfac14lem  23739  txdis1cn  23757  hausdiag  23767  txkgen  23774  qtopval2  23818  basqtop  23833  qtopcld  23835  qtopeu  23838  qtoprest  23839  imastopn  23842  hmeontr  23891  hmeoimaf1o  23892  cmphaushmeo  23922  ordthmeolem  23923  elfm3  24072  rnelfmlem  24074  rnelfm  24075  alexsubALTlem4  24172  cldsubg  24233  tgpconncompeqg  24234  tgpconncomp  24235  qustgpopn  24242  qustgplem  24243  tsmsf1o  24267  ucncn  24406  imasf1oxms  24611  blcld  24627  metustfbas  24679  cfilucfil  24681  metuel2  24687  icchmeo  25065  relcmpcmet  25442  minveclem4a  25554  nulmbl2  25660  icombl  25688  ioombl  25689  uniiccdif  25702  volivth  25731  mbfres2  25769  itg1addlem5  25824  itgsplitioo  25962  dvcobr  26070  dvcnvlem  26100  lhop1lem  26137  lhop  26140  dvcnvrelem2  26142  uc1pval  26262  mon1pval  26264  vieta1lem2  26437  basellem5  27211  onnolt  28421  f1otrg  29157  axlowdimlem13  29241  axcontlem10  29260  uhgrspansubgr  29578  vtxdun  29768  pthdlem1  30052  eucrct2eupth  30533  ssmd1  32600  mdslj2i  32609  atcvat4i  32686  imadifxp  32883  nfpconfp  32914  2ndresdju  32931  ofpreima  32947  ofpreima2  32948  fsuppcurry1  33006  fsuppcurry2  33007  indpreima  33122  indf1ofs  33123  ccatws1f1olast  33209  gsumpart  33320  symgcom  33340  symgcom2  33341  pmtrcnel  33346  cycpmfvlem  33369  cycpmfv3  33372  elrgspnsubrunlem2  33505  elrspunidl  33676  idlinsubrg  33679  esplymhp  33899  esplyfval1  33904  esplyfvaln  33905  fldextrspunlsp  34005  qtophaus  34167  reff  34170  locfinreflem  34171  zarcmplem  34212  hauseqcn  34229  oms0  34628  eulerpartlemv  34695  eulerpartlemb  34699  eulerpartlemr  34705  eulerpartlemgs2  34711  eulerpartlemn  34712  ballotlemro  34854  bnj1253  35346  bnj1280  35349  onvfowev  35495  pthhashvtx  35515  acycgr0v  35535  prclisacycgr  35538  subfacp1lem3  35569  cvmscld  35660  cvmsss2  35661  cvmliftmolem1  35668  cvmliftlem7  35678  cvmlift2lem9  35698  cvmlift3lem7  35712  fnessref  36753  tailf  36771  poimirlem3  38157  mbfresfi  38200  cnambfre  38202  itg2addnclem2  38206  mettrifi  38291  ismtyres  38342  isdrngo2  38492  press  39033  diaintclN  41717  dibintclN  41826  dihintcl  42003  dochocss  42025  mapdunirnN  42309  pw2f1ocnv  43651  wessf1ornlem  45790  monoord2xrv  46084  itgcoscmulx  46570  ibliooicc  46572  stoweidlem11  46612  stoweidlem34  46635  fourierdlem48  46755  fourierdlem49  46756  fourierdlem74  46781  uniimaprimaeqfv  48015  elsetpreimafvssdm  48019  fdivmptf  49201  refdivmptf  49202  iscnrm3llem2  49608  imaidfu  49768