Theorem sseqtrid 3989

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

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

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 2701

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

This theorem is referenced by:  sseqtrrid  3990  iunxdif3  5059  fssdm  6707  fndmdif  7014  fneqeql2  7019  fconst4  7188  isofrlem  7315  fvmptopab  7443  f1opw2  7644  fparlem3  8093  fparlem4  8094  fnwelem  8110  fsuppeq  8154  fsuppeqg  8155  ecss  8722  pw2f1olem  9045  fopwdom  9049  ssenen  9115  ssfiALT  9138  fiint  9277  fiintOLD  9278  f1opwfi  9307  kmlem5  10108  enfin2i  10274  fpwwe2lem5  10588  fpwwe2lem8  10591  tskuni  10736  monoord2  13998  seqz  14015  cshimadifsn0  14796  binom1dif  15799  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  bitsres  16443  prdshom  17430  imasless  17503  cntzval  19253  f1omvdmvd  19373  f1omvdconj  19376  pmtrfb  19395  symggen  19400  symggen2  19401  psgnunilem1  19423  gsumzaddlem  19851  rngcbas  20530  ringcbas  20559  isdrngd  20674  isdrngdOLD  20676  lspextmo  20963  znleval  21464  freshmansdream  21484  ordtcld1  23084  ordtcld2  23085  cnpnei  23151  cnntri  23158  cncls2  23160  cncls  23161  cnntr  23162  cncnp  23167  cndis  23178  paste  23181  cmpfi  23295  conncompcld  23321  1stcfb  23332  1stccnp  23349  cldllycmp  23382  llycmpkgen2  23437  kgencn  23443  kgencn3  23445  dfac14lem  23504  txdis1cn  23522  hausdiag  23532  txkgen  23539  qtopval2  23583  basqtop  23598  qtopcld  23600  qtopeu  23603  qtoprest  23604  imastopn  23607  hmeontr  23656  hmeoimaf1o  23657  cmphaushmeo  23687  ordthmeolem  23688  elfm3  23837  rnelfmlem  23839  rnelfm  23840  alexsubALTlem4  23937  cldsubg  23998  tgpconncompeqg  23999  tgpconncomp  24000  qustgpopn  24007  qustgplem  24008  tsmsf1o  24032  ucncn  24172  imasf1oxms  24377  blcld  24393  metustfbas  24445  cfilucfil  24447  metuel2  24453  icchmeo  24838  icchmeoOLD  24839  relcmpcmet  25218  minveclem4a  25330  nulmbl2  25437  icombl  25465  ioombl  25466  uniiccdif  25479  volivth  25508  mbfres2  25546  itg1addlem5  25601  itgsplitioo  25739  dvcobr  25849  dvcobrOLD  25850  dvcnvlem  25880  lhop1lem  25918  lhop  25921  dvcnvrelem2  25923  uc1pval  26045  mon1pval  26047  vieta1lem2  26219  basellem5  26995  onnolt  28167  f1otrg  28798  axlowdimlem13  28881  axcontlem10  28900  uhgrspansubgr  29218  vtxdun  29409  pthdlem1  29696  eucrct2eupth  30174  ssmd1  32240  mdslj2i  32249  atcvat4i  32326  imadifxp  32530  nfpconfp  32556  2ndresdju  32573  ofpreima  32589  ofpreima2  32590  fsuppcurry1  32648  fsuppcurry2  32649  indpreima  32788  indf1ofs  32789  ccatws1f1olast  32874  gsumpart  32997  symgcom  33040  symgcom2  33041  pmtrcnel  33046  cycpmfvlem  33069  cycpmfv3  33072  elrgspnsubrunlem2  33199  elrspunidl  33399  idlinsubrg  33402  fldextrspunlsp  33669  qtophaus  33826  reff  33829  locfinreflem  33830  zarcmplem  33871  hauseqcn  33888  oms0  34288  eulerpartlemv  34355  eulerpartlemb  34359  eulerpartlemr  34365  eulerpartlemgs2  34371  eulerpartlemn  34372  ballotlemro  34514  bnj1253  35007  bnj1280  35010  pthhashvtx  35115  acycgr0v  35135  prclisacycgr  35138  subfacp1lem3  35169  cvmscld  35260  cvmsss2  35261  cvmliftmolem1  35268  cvmliftlem7  35278  cvmlift2lem9  35298  cvmlift3lem7  35312  fnessref  36345  tailf  36363  poimirlem3  37617  mbfresfi  37660  cnambfre  37662  itg2addnclem2  37666  mettrifi  37751  ismtyres  37802  isdrngo2  37952  diaintclN  41052  dibintclN  41161  dihintcl  41338  dochocss  41360  mapdunirnN  41644  pw2f1ocnv  43026  wessf1ornlem  45179  monoord2xrv  45479  itgcoscmulx  45967  ibliooicc  45969  stoweidlem11  46009  stoweidlem34  46032  fourierdlem48  46152  fourierdlem49  46153  fourierdlem74  46178  uniimaprimaeqfv  47383  elsetpreimafvssdm  47387  fdivmptf  48530  refdivmptf  48531  iscnrm3llem2  48938  imaidfu  49099