Theorem sseqtrid 3964

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  sseqtrrid  3965  iunxdif3  5037  fssdm  6687  fndmdif  6994  fneqeql2  6999  fconst4  7169  isofrlem  7295  fvmptopab  7422  f1opw2  7622  fparlem3  8064  fparlem4  8065  fnwelem  8081  fsuppeq  8125  fsuppeqg  8126  ecss  8695  pw2f1olem  9019  fopwdom  9023  ssenen  9089  ssfiALT  9108  fiint  9237  f1opwfi  9266  kmlem5  10077  enfin2i  10243  fpwwe2lem5  10558  fpwwe2lem8  10561  tskuni  10706  monoord2  13995  seqz  14012  cshimadifsn0  14792  binom1dif  15798  bpolycl  16017  bpolysum  16018  bpolydiflem  16019  bitsres  16442  prdshom  17430  imasless  17504  cntzval  19296  f1omvdmvd  19418  f1omvdconj  19421  pmtrfb  19440  symggen  19445  symggen2  19446  psgnunilem1  19468  gsumzaddlem  19896  rngcbas  20598  ringcbas  20627  isdrngd  20742  isdrngdOLD  20744  lspextmo  21051  znleval  21534  freshmansdream  21554  ordtcld1  23162  ordtcld2  23163  cnpnei  23229  cnntri  23236  cncls2  23238  cncls  23239  cnntr  23240  cncnp  23245  cndis  23256  paste  23259  cmpfi  23373  conncompcld  23399  1stcfb  23410  1stccnp  23427  cldllycmp  23460  llycmpkgen2  23515  kgencn  23521  kgencn3  23523  dfac14lem  23582  txdis1cn  23600  hausdiag  23610  txkgen  23617  qtopval2  23661  basqtop  23676  qtopcld  23678  qtopeu  23681  qtoprest  23682  imastopn  23685  hmeontr  23734  hmeoimaf1o  23735  cmphaushmeo  23765  ordthmeolem  23766  elfm3  23915  rnelfmlem  23917  rnelfm  23918  alexsubALTlem4  24015  cldsubg  24076  tgpconncompeqg  24077  tgpconncomp  24078  qustgpopn  24085  qustgplem  24086  tsmsf1o  24110  ucncn  24249  imasf1oxms  24454  blcld  24470  metustfbas  24522  cfilucfil  24524  metuel2  24530  icchmeo  24908  relcmpcmet  25285  minveclem4a  25397  nulmbl2  25503  icombl  25531  ioombl  25532  uniiccdif  25545  volivth  25574  mbfres2  25612  itg1addlem5  25667  itgsplitioo  25805  dvcobr  25913  dvcnvlem  25943  lhop1lem  25980  lhop  25983  dvcnvrelem2  25985  uc1pval  26105  mon1pval  26107  vieta1lem2  26277  basellem5  27048  onnolt  28258  f1otrg  28939  axlowdimlem13  29023  axcontlem10  29042  uhgrspansubgr  29360  vtxdun  29550  pthdlem1  29834  eucrct2eupth  30315  ssmd1  32382  mdslj2i  32391  atcvat4i  32468  imadifxp  32671  nfpconfp  32705  2ndresdju  32722  ofpreima  32738  ofpreima2  32739  fsuppcurry1  32797  fsuppcurry2  32798  indpreima  32925  indf1ofs  32926  ccatws1f1olast  33012  gsumpart  33124  symgcom  33144  symgcom2  33145  pmtrcnel  33150  cycpmfvlem  33173  cycpmfv3  33176  elrgspnsubrunlem2  33309  elrspunidl  33488  idlinsubrg  33491  esplymhp  33712  esplyfval1  33717  esplyfvaln  33718  fldextrspunlsp  33818  qtophaus  33980  reff  33983  locfinreflem  33984  zarcmplem  34025  hauseqcn  34042  oms0  34441  eulerpartlemv  34508  eulerpartlemb  34512  eulerpartlemr  34518  eulerpartlemgs2  34524  eulerpartlemn  34525  ballotlemro  34667  bnj1253  35159  bnj1280  35162  pthhashvtx  35310  acycgr0v  35330  prclisacycgr  35333  subfacp1lem3  35364  cvmscld  35455  cvmsss2  35456  cvmliftmolem1  35463  cvmliftlem7  35473  cvmlift2lem9  35493  cvmlift3lem7  35507  fnessref  36539  tailf  36557  poimirlem3  37944  mbfresfi  37987  cnambfre  37989  itg2addnclem2  37993  mettrifi  38078  ismtyres  38129  isdrngo2  38279  press  38820  diaintclN  41504  dibintclN  41613  dihintcl  41790  dochocss  41812  mapdunirnN  42096  pw2f1ocnv  43465  wessf1ornlem  45615  monoord2xrv  45911  itgcoscmulx  46397  ibliooicc  46399  stoweidlem11  46439  stoweidlem34  46462  fourierdlem48  46582  fourierdlem49  46583  fourierdlem74  46608  uniimaprimaeqfv  47842  elsetpreimafvssdm  47846  fdivmptf  49017  refdivmptf  49018  iscnrm3llem2  49425  imaidfu  49585