Theorem sseqtrid 3955

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  sseqtrrid  3956  iunxdif3  5058  fssdm  6754  fndmdif  7067  fneqeql2  7072  fconst4  7246  isofrlem  7374  fvmptopab  7501  f1opw2  7703  fparlem3  8155  fparlem4  8156  fnwelem  8173  fsuppeq  8223  fsuppeqg  8224  ecss  8800  pw2f1olem  9131  fopwdom  9135  ssenen  9201  ssfiALT  9220  fiint  9349  f1opwfi  9376  kmlem5  10263  enfin2i  10429  fpwwe2lem5  10750  fpwwe2lem8  10753  tskuni  10898  monoord2  14206  seqz  14223  cshimadifsn0  15012  binom1dif  16034  bpolycl  16250  bpolysum  16251  bpolydiflem  16252  bitsres  16675  prdshom  17670  imasless  17744  cntzval  19568  f1omvdmvd  19690  f1omvdconj  19693  pmtrfb  19712  symggen  19717  symggen2  19718  psgnunilem1  19740  gsumzaddlem  20168  rngcbas  20906  ringcbas  20935  isdrngd  21055  isdrngdOLD  21057  lspextmo  21364  znleval  21893  freshmansdream  21913  ordtcld1  23548  ordtcld2  23549  cnpnei  23615  cnntri  23622  cncls2  23624  cncls  23625  cnntr  23626  cncnp  23631  cndis  23642  paste  23645  cmpfi  23759  conncompcld  23785  1stcfb  23796  1stccnp  23814  cldllycmp  23847  llycmpkgen2  23902  kgencn  23908  kgencn3  23910  dfac14lem  23969  txdis1cn  23987  hausdiag  23997  txkgen  24004  qtopval2  24048  basqtop  24063  qtopcld  24065  qtopeu  24068  qtoprest  24069  imastopn  24072  hmeontr  24121  hmeoimaf1o  24122  cmphaushmeo  24152  ordthmeolem  24153  elfm3  24302  rnelfmlem  24304  rnelfm  24305  alexsubALTlem4  24402  cldsubg  24463  tgpconncompeqg  24464  tgpconncomp  24465  qustgpopn  24472  qustgplem  24473  tsmsf1o  24497  ucncn  24636  imasf1oxms  24841  blcld  24857  metustfbas  24909  cfilucfil  24911  metuel2  24917  icchmeo  25295  relcmpcmet  25672  minveclem4a  25784  nulmbl2  25890  icombl  25918  ioombl  25919  uniiccdif  25932  volivth  25961  mbfres2  25999  itg1addlem5  26054  itgsplitioo  26191  dvcobr  26299  dvcnvlem  26329  lhop1lem  26366  lhop  26369  dvcnvrelem2  26371  uc1pval  26491  mon1pval  26493  vieta1lem2  26667  basellem5  27445  onnolt  28685  f1otrg  29481  axlowdimlem13  29565  axcontlem10  29584  uhgrspansubgr  29905  vtxdun  30095  pthhashvtx  30348  pthdlem1  30385  eucrct2eupth  30879  ssmd1  32946  mdslj2i  32955  atcvat4i  33032  imadifxp  33270  nfpconfp  33301  2ndresdju  33318  ofpreima  33334  ofpreima2  33335  fsuppcurry1  33389  fsuppcurry2  33390  indpreima  33505  indf1ofs  33506  ccatws1f1olast  33588  gsumpart  33700  symgcom  33720  symgcom2  33721  pmtrcnel  33726  cycpmfvlem  33749  cycpmfv3  33752  elrgspnsubrunlem2  33885  elrspunidl  34062  idlinsubrg  34065  esplymhp  34283  esplyfval1  34288  esplyfvaln  34289  fldextrspunlsp  34389  qtophaus  34551  locfinreflem  34555  zarcmplem  34596  hauseqcn  34613  oms0  35012  eulerpartlemv  35079  eulerpartlemb  35083  eulerpartlemr  35089  eulerpartlemgs2  35095  eulerpartlemn  35096  ballotlemro  35238  bnj1253  35730  bnj1280  35733  onvfowev  36063  acycgr0v  36083  prclisacycgr  36086  subfacp1lem3  36127  cvmscld  36218  cvmsss2  36219  cvmliftmolem1  36226  cvmliftlem7  36236  cvmlift2lem9  36256  cvmlift3lem7  36270  fnessref  37336  tailf  37354  poimirlem3  38746  mbfresfi  38789  cnambfre  38791  itg2addnclem2  38795  mettrifi  38894  ismtyres  38945  isdrngo2  39095  press  39634  diaintclN  42318  dibintclN  42427  dihintcl  42604  dochocss  42626  mapdunirnN  42910  pw2f1ocnv  44248  wessf1ornlem  46415  monoord2xrv  46708  itgcoscmulx  47194  ibliooicc  47196  stoweidlem11  47236  stoweidlem34  47259  fourierdlem48  47379  fourierdlem49  47380  fourierdlem74  47405  tmachlem-agreeprod  48162  uniimaprimaeqfv  48679  elsetpreimafvssdm  48683  fdivmptf  49868  refdivmptf  49869  iscnrm3llem2  50279  imaidfu  50441