Theorem sseqtrid 4034

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3948

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  sseqtrrid  4035  iunxdif3  5098  fssdm  6737  fndmdif  7043  fneqeql2  7048  fconst4  7218  isofrlem  7340  fvmptopab  7466  f1opw2  7664  fparlem3  8103  fparlem4  8104  fnwelem  8120  fsuppeq  8163  fsuppeqg  8164  ecss  8752  pw2f1olem  9079  fopwdom  9083  ssenen  9154  ssfiALT  9177  phplem2OLD  9221  fiint  9327  f1opwfi  9359  kmlem5  10152  enfin2i  10319  fpwwe2lem5  10633  fpwwe2lem8  10636  tskuni  10781  monoord2  14004  seqz  14021  cshimadifsn0  14786  binom1dif  15784  bpolycl  16001  bpolysum  16002  bpolydiflem  16003  bitsres  16419  prdshom  17418  imasless  17491  cntzval  19227  f1omvdmvd  19353  f1omvdconj  19356  pmtrfb  19375  symggen  19380  symggen2  19381  psgnunilem1  19403  gsumzaddlem  19831  isdrngd  20534  isdrngdOLD  20536  lspextmo  20812  znleval  21330  ordtcld1  22922  ordtcld2  22923  cnpnei  22989  cnntri  22996  cncls2  22998  cncls  22999  cnntr  23000  cncnp  23005  cndis  23016  paste  23019  cmpfi  23133  conncompcld  23159  1stcfb  23170  1stccnp  23187  cldllycmp  23220  llycmpkgen2  23275  kgencn  23281  kgencn3  23283  dfac14lem  23342  txdis1cn  23360  hausdiag  23370  txkgen  23377  qtopval2  23421  basqtop  23436  qtopcld  23438  qtopeu  23441  qtoprest  23442  imastopn  23445  hmeontr  23494  hmeoimaf1o  23495  cmphaushmeo  23525  ordthmeolem  23526  elfm3  23675  rnelfmlem  23677  rnelfm  23678  alexsubALTlem4  23775  cldsubg  23836  tgpconncompeqg  23837  tgpconncomp  23838  qustgpopn  23845  qustgplem  23846  tsmsf1o  23870  ucncn  24011  imasf1oxms  24219  blcld  24235  metustfbas  24287  cfilucfil  24289  metuel2  24295  icchmeo  24686  icchmeoOLD  24687  relcmpcmet  25067  minveclem4a  25179  nulmbl2  25286  icombl  25314  ioombl  25315  uniiccdif  25328  volivth  25357  mbfres2  25395  itg1addlem5  25451  itgsplitioo  25588  dvcobr  25698  dvcobrOLD  25699  dvcnvlem  25729  lhop1lem  25766  lhop  25769  dvcnvrelem2  25771  uc1pval  25893  mon1pval  25895  vieta1lem2  26061  basellem5  26826  f1otrg  28390  axlowdimlem13  28480  axcontlem10  28499  uhgrspansubgr  28816  vtxdun  29006  pthdlem1  29291  eucrct2eupth  29766  ssmd1  31832  mdslj2i  31841  atcvat4i  31918  imadifxp  32100  nfpconfp  32124  2ndresdju  32142  ofpreima  32158  ofpreima2  32159  fsuppcurry1  32218  fsuppcurry2  32219  gsumpart  32478  symgcom  32515  symgcom2  32516  pmtrcnel  32521  cycpmfvlem  32542  cycpmfv3  32545  freshmansdream  32652  elrspunidl  32821  idlinsubrg  32824  qtophaus  33115  reff  33118  locfinreflem  33119  zarcmplem  33160  hauseqcn  33177  indpreima  33322  indf1ofs  33323  oms0  33595  eulerpartlemv  33662  eulerpartlemb  33666  eulerpartlemr  33672  eulerpartlemgs2  33678  eulerpartlemn  33679  ballotlemro  33820  bnj1253  34327  bnj1280  34330  pthhashvtx  34417  acycgr0v  34438  prclisacycgr  34441  subfacp1lem3  34472  cvmscld  34563  cvmsss2  34564  cvmliftmolem1  34571  cvmliftlem7  34581  cvmlift2lem9  34601  cvmlift3lem7  34615  fnessref  35546  tailf  35564  poimirlem3  36795  mbfresfi  36838  cnambfre  36840  itg2addnclem2  36844  mettrifi  36929  ismtyres  36980  isdrngo2  37130  diaintclN  40233  dibintclN  40342  dihintcl  40519  dochocss  40541  mapdunirnN  40825  pw2f1ocnv  42079  wessf1ornlem  44183  monoord2xrv  44493  itgcoscmulx  44984  ibliooicc  44986  stoweidlem11  45026  stoweidlem34  45049  fourierdlem48  45169  fourierdlem49  45170  fourierdlem74  45195  uniimaprimaeqfv  46349  elsetpreimafvssdm  46353  rngcbas  46952  ringcbas  46998  fdivmptf  47315  refdivmptf  47316  iscnrm3llem2  47671