Theorem sseqtrid 4006

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948

This theorem is referenced by:  sseqtrrid  4007  iunxdif3  5076  fssdm  6730  fndmdif  7037  fneqeql2  7042  fconst4  7211  isofrlem  7338  fvmptopab  7466  f1opw2  7667  fparlem3  8118  fparlem4  8119  fnwelem  8135  fsuppeq  8179  fsuppeqg  8180  ecss  8772  pw2f1olem  9095  fopwdom  9099  ssenen  9170  ssfiALT  9193  phplem2OLD  9234  fiint  9343  fiintOLD  9344  f1opwfi  9373  kmlem5  10174  enfin2i  10340  fpwwe2lem5  10654  fpwwe2lem8  10657  tskuni  10802  monoord2  14056  seqz  14073  cshimadifsn0  14854  binom1dif  15854  bpolycl  16073  bpolysum  16074  bpolydiflem  16075  bitsres  16497  prdshom  17486  imasless  17559  cntzval  19309  f1omvdmvd  19429  f1omvdconj  19432  pmtrfb  19451  symggen  19456  symggen2  19457  psgnunilem1  19479  gsumzaddlem  19907  rngcbas  20586  ringcbas  20615  isdrngd  20730  isdrngdOLD  20732  lspextmo  21019  znleval  21520  freshmansdream  21540  ordtcld1  23140  ordtcld2  23141  cnpnei  23207  cnntri  23214  cncls2  23216  cncls  23217  cnntr  23218  cncnp  23223  cndis  23234  paste  23237  cmpfi  23351  conncompcld  23377  1stcfb  23388  1stccnp  23405  cldllycmp  23438  llycmpkgen2  23493  kgencn  23499  kgencn3  23501  dfac14lem  23560  txdis1cn  23578  hausdiag  23588  txkgen  23595  qtopval2  23639  basqtop  23654  qtopcld  23656  qtopeu  23659  qtoprest  23660  imastopn  23663  hmeontr  23712  hmeoimaf1o  23713  cmphaushmeo  23743  ordthmeolem  23744  elfm3  23893  rnelfmlem  23895  rnelfm  23896  alexsubALTlem4  23993  cldsubg  24054  tgpconncompeqg  24055  tgpconncomp  24056  qustgpopn  24063  qustgplem  24064  tsmsf1o  24088  ucncn  24228  imasf1oxms  24433  blcld  24449  metustfbas  24501  cfilucfil  24503  metuel2  24509  icchmeo  24894  icchmeoOLD  24895  relcmpcmet  25275  minveclem4a  25387  nulmbl2  25494  icombl  25522  ioombl  25523  uniiccdif  25536  volivth  25565  mbfres2  25603  itg1addlem5  25658  itgsplitioo  25796  dvcobr  25906  dvcobrOLD  25907  dvcnvlem  25937  lhop1lem  25975  lhop  25978  dvcnvrelem2  25980  uc1pval  26102  mon1pval  26104  vieta1lem2  26276  basellem5  27052  onnolt  28224  f1otrg  28855  axlowdimlem13  28938  axcontlem10  28957  uhgrspansubgr  29275  vtxdun  29466  pthdlem1  29753  eucrct2eupth  30231  ssmd1  32297  mdslj2i  32306  atcvat4i  32383  imadifxp  32587  nfpconfp  32615  2ndresdju  32632  ofpreima  32648  ofpreima2  32649  fsuppcurry1  32707  fsuppcurry2  32708  indpreima  32847  indf1ofs  32848  ccatws1f1olast  32933  gsumpart  33056  symgcom  33099  symgcom2  33100  pmtrcnel  33105  cycpmfvlem  33128  cycpmfv3  33131  elrgspnsubrunlem2  33248  elrspunidl  33448  idlinsubrg  33451  fldextrspunlsp  33720  qtophaus  33872  reff  33875  locfinreflem  33876  zarcmplem  33917  hauseqcn  33934  oms0  34334  eulerpartlemv  34401  eulerpartlemb  34405  eulerpartlemr  34411  eulerpartlemgs2  34417  eulerpartlemn  34418  ballotlemro  34560  bnj1253  35053  bnj1280  35056  pthhashvtx  35155  acycgr0v  35175  prclisacycgr  35178  subfacp1lem3  35209  cvmscld  35300  cvmsss2  35301  cvmliftmolem1  35308  cvmliftlem7  35318  cvmlift2lem9  35338  cvmlift3lem7  35352  fnessref  36380  tailf  36398  poimirlem3  37652  mbfresfi  37695  cnambfre  37697  itg2addnclem2  37701  mettrifi  37786  ismtyres  37837  isdrngo2  37987  diaintclN  41082  dibintclN  41191  dihintcl  41368  dochocss  41390  mapdunirnN  41674  pw2f1ocnv  43036  wessf1ornlem  45189  monoord2xrv  45490  itgcoscmulx  45978  ibliooicc  45980  stoweidlem11  46020  stoweidlem34  46043  fourierdlem48  46163  fourierdlem49  46164  fourierdlem74  46189  uniimaprimaeqfv  47376  elsetpreimafvssdm  47380  fdivmptf  48501  refdivmptf  48502  iscnrm3llem2  48904  imaidfu  49049