Theorem sseqtrid 3976

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  sseqtrrid  3977  iunxdif3  5050  fssdm  6681  fndmdif  6987  fneqeql2  6992  fconst4  7160  isofrlem  7286  fvmptopab  7413  f1opw2  7613  fparlem3  8056  fparlem4  8057  fnwelem  8073  fsuppeq  8117  fsuppeqg  8118  ecss  8686  pw2f1olem  9009  fopwdom  9013  ssenen  9079  ssfiALT  9098  fiint  9227  f1opwfi  9256  kmlem5  10065  enfin2i  10231  fpwwe2lem5  10546  fpwwe2lem8  10549  tskuni  10694  monoord2  13956  seqz  13973  cshimadifsn0  14753  binom1dif  15756  bpolycl  15975  bpolysum  15976  bpolydiflem  15977  bitsres  16400  prdshom  17387  imasless  17461  cntzval  19250  f1omvdmvd  19372  f1omvdconj  19375  pmtrfb  19394  symggen  19399  symggen2  19400  psgnunilem1  19422  gsumzaddlem  19850  rngcbas  20554  ringcbas  20583  isdrngd  20698  isdrngdOLD  20700  lspextmo  21008  znleval  21509  freshmansdream  21529  ordtcld1  23141  ordtcld2  23142  cnpnei  23208  cnntri  23215  cncls2  23217  cncls  23218  cnntr  23219  cncnp  23224  cndis  23235  paste  23238  cmpfi  23352  conncompcld  23378  1stcfb  23389  1stccnp  23406  cldllycmp  23439  llycmpkgen2  23494  kgencn  23500  kgencn3  23502  dfac14lem  23561  txdis1cn  23579  hausdiag  23589  txkgen  23596  qtopval2  23640  basqtop  23655  qtopcld  23657  qtopeu  23660  qtoprest  23661  imastopn  23664  hmeontr  23713  hmeoimaf1o  23714  cmphaushmeo  23744  ordthmeolem  23745  elfm3  23894  rnelfmlem  23896  rnelfm  23897  alexsubALTlem4  23994  cldsubg  24055  tgpconncompeqg  24056  tgpconncomp  24057  qustgpopn  24064  qustgplem  24065  tsmsf1o  24089  ucncn  24228  imasf1oxms  24433  blcld  24449  metustfbas  24501  cfilucfil  24503  metuel2  24509  icchmeo  24894  icchmeoOLD  24895  relcmpcmet  25274  minveclem4a  25386  nulmbl2  25493  icombl  25521  ioombl  25522  uniiccdif  25535  volivth  25564  mbfres2  25602  itg1addlem5  25657  itgsplitioo  25795  dvcobr  25905  dvcobrOLD  25906  dvcnvlem  25936  lhop1lem  25974  lhop  25977  dvcnvrelem2  25979  uc1pval  26101  mon1pval  26103  vieta1lem2  26275  basellem5  27051  onnolt  28262  f1otrg  28943  axlowdimlem13  29027  axcontlem10  29046  uhgrspansubgr  29364  vtxdun  29555  pthdlem1  29839  eucrct2eupth  30320  ssmd1  32386  mdslj2i  32395  atcvat4i  32472  imadifxp  32676  nfpconfp  32710  2ndresdju  32727  ofpreima  32743  ofpreima2  32744  fsuppcurry1  32803  fsuppcurry2  32804  indpreima  32947  indf1ofs  32948  ccatws1f1olast  33034  gsumpart  33146  symgcom  33165  symgcom2  33166  pmtrcnel  33171  cycpmfvlem  33194  cycpmfv3  33197  elrgspnsubrunlem2  33330  elrspunidl  33509  idlinsubrg  33512  esplymhp  33726  fldextrspunlsp  33831  qtophaus  33993  reff  33996  locfinreflem  33997  zarcmplem  34038  hauseqcn  34055  oms0  34454  eulerpartlemv  34521  eulerpartlemb  34525  eulerpartlemr  34531  eulerpartlemgs2  34537  eulerpartlemn  34538  ballotlemro  34680  bnj1253  35173  bnj1280  35176  pthhashvtx  35322  acycgr0v  35342  prclisacycgr  35345  subfacp1lem3  35376  cvmscld  35467  cvmsss2  35468  cvmliftmolem1  35475  cvmliftlem7  35485  cvmlift2lem9  35505  cvmlift3lem7  35519  fnessref  36551  tailf  36569  poimirlem3  37820  mbfresfi  37863  cnambfre  37865  itg2addnclem2  37869  mettrifi  37954  ismtyres  38005  isdrngo2  38155  press  38668  diaintclN  41314  dibintclN  41423  dihintcl  41600  dochocss  41622  mapdunirnN  41906  pw2f1ocnv  43275  wessf1ornlem  45425  monoord2xrv  45723  itgcoscmulx  46209  ibliooicc  46211  stoweidlem11  46251  stoweidlem34  46274  fourierdlem48  46394  fourierdlem49  46395  fourierdlem74  46420  uniimaprimaeqfv  47624  elsetpreimafvssdm  47628  fdivmptf  48783  refdivmptf  48784  iscnrm3llem2  49191  imaidfu  49351