Theorem sseqtrid 3978

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sseqtrrid  3979  iunxdif3  5051  fssdm  6707  fndmdif  7019  fneqeql2  7024  fconst4  7194  isofrlem  7320  fvmptopab  7447  f1opw2  7647  fparlem3  8088  fparlem4  8089  fnwelem  8106  fsuppeq  8150  fsuppeqg  8151  ecss  8725  pw2f1olem  9049  fopwdom  9053  ssenen  9119  ssfiALT  9138  fiint  9267  f1opwfi  9296  kmlem5  10108  enfin2i  10275  fpwwe2lem5  10590  fpwwe2lem8  10593  tskuni  10738  monoord2  14043  seqz  14060  cshimadifsn0  14840  binom1dif  15846  bpolycl  16065  bpolysum  16066  bpolydiflem  16067  bitsres  16490  prdshom  17479  imasless  17553  cntzval  19344  f1omvdmvd  19466  f1omvdconj  19469  pmtrfb  19488  symggen  19493  symggen2  19494  psgnunilem1  19516  gsumzaddlem  19944  rngcbas  20650  ringcbas  20679  isdrngd  20794  isdrngdOLD  20796  lspextmo  21103  znleval  21586  freshmansdream  21606  ordtcld1  23237  ordtcld2  23238  cnpnei  23304  cnntri  23311  cncls2  23313  cncls  23314  cnntr  23315  cncnp  23320  cndis  23331  paste  23334  cmpfi  23448  conncompcld  23474  1stcfb  23485  1stccnp  23502  cldllycmp  23535  llycmpkgen2  23590  kgencn  23596  kgencn3  23598  dfac14lem  23657  txdis1cn  23675  hausdiag  23685  txkgen  23692  qtopval2  23736  basqtop  23751  qtopcld  23753  qtopeu  23756  qtoprest  23757  imastopn  23760  hmeontr  23809  hmeoimaf1o  23810  cmphaushmeo  23840  ordthmeolem  23841  elfm3  23990  rnelfmlem  23992  rnelfm  23993  alexsubALTlem4  24090  cldsubg  24151  tgpconncompeqg  24152  tgpconncomp  24153  qustgpopn  24160  qustgplem  24161  tsmsf1o  24185  ucncn  24324  imasf1oxms  24529  blcld  24545  metustfbas  24597  cfilucfil  24599  metuel2  24605  icchmeo  24983  relcmpcmet  25360  minveclem4a  25472  nulmbl2  25578  icombl  25606  ioombl  25607  uniiccdif  25620  volivth  25649  mbfres2  25687  itg1addlem5  25742  itgsplitioo  25880  dvcobr  25988  dvcnvlem  26018  lhop1lem  26055  lhop  26058  dvcnvrelem2  26060  uc1pval  26180  mon1pval  26182  vieta1lem2  26352  basellem5  27126  onnolt  28336  f1otrg  29017  axlowdimlem13  29101  axcontlem10  29120  uhgrspansubgr  29438  vtxdun  29628  pthdlem1  29912  eucrct2eupth  30393  ssmd1  32460  mdslj2i  32469  atcvat4i  32546  imadifxp  32750  nfpconfp  32784  2ndresdju  32801  ofpreima  32817  ofpreima2  32818  fsuppcurry1  32876  fsuppcurry2  32877  indpreima  33004  indf1ofs  33005  ccatws1f1olast  33091  gsumpart  33204  symgcom  33224  symgcom2  33225  pmtrcnel  33230  cycpmfvlem  33253  cycpmfv3  33256  elrgspnsubrunlem2  33390  elrspunidl  33575  idlinsubrg  33578  esplymhp  33826  esplyfval1  33831  esplyfvaln  33832  fldextrspunlsp  33932  qtophaus  34094  reff  34097  locfinreflem  34098  zarcmplem  34139  hauseqcn  34156  oms0  34555  eulerpartlemv  34622  eulerpartlemb  34626  eulerpartlemr  34632  eulerpartlemgs2  34638  eulerpartlemn  34639  ballotlemro  34781  bnj1253  35276  bnj1280  35279  onvfowev  35423  pthhashvtx  35442  acycgr0v  35462  prclisacycgr  35465  subfacp1lem3  35496  cvmscld  35587  cvmsss2  35588  cvmliftmolem1  35595  cvmliftlem7  35605  cvmlift2lem9  35625  cvmlift3lem7  35639  fnessref  36681  tailf  36699  poimirlem3  38086  mbfresfi  38129  cnambfre  38131  itg2addnclem2  38135  mettrifi  38220  ismtyres  38271  isdrngo2  38421  press  38962  diaintclN  41646  dibintclN  41755  dihintcl  41932  dochocss  41954  mapdunirnN  42238  pw2f1ocnv  43578  wessf1ornlem  45727  monoord2xrv  46021  itgcoscmulx  46507  ibliooicc  46509  stoweidlem11  46549  stoweidlem34  46572  fourierdlem48  46692  fourierdlem49  46693  fourierdlem74  46718  uniimaprimaeqfv  47952  elsetpreimafvssdm  47956  fdivmptf  49127  refdivmptf  49128  iscnrm3llem2  49535  imaidfu  49695