Theorem sseqtrid 3973

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

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

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 2705

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

This theorem is referenced by:  sseqtrrid  3974  iunxdif3  5045  fssdm  6675  fndmdif  6981  fneqeql2  6986  fconst4  7154  isofrlem  7280  fvmptopab  7407  f1opw2  7607  fparlem3  8050  fparlem4  8051  fnwelem  8067  fsuppeq  8111  fsuppeqg  8112  ecss  8679  pw2f1olem  9001  fopwdom  9005  ssenen  9071  ssfiALT  9090  fiint  9218  f1opwfi  9247  kmlem5  10053  enfin2i  10219  fpwwe2lem5  10533  fpwwe2lem8  10536  tskuni  10681  monoord2  13942  seqz  13959  cshimadifsn0  14739  binom1dif  15742  bpolycl  15961  bpolysum  15962  bpolydiflem  15963  bitsres  16386  prdshom  17373  imasless  17446  cntzval  19235  f1omvdmvd  19357  f1omvdconj  19360  pmtrfb  19379  symggen  19384  symggen2  19385  psgnunilem1  19407  gsumzaddlem  19835  rngcbas  20538  ringcbas  20567  isdrngd  20682  isdrngdOLD  20684  lspextmo  20992  znleval  21493  freshmansdream  21513  ordtcld1  23113  ordtcld2  23114  cnpnei  23180  cnntri  23187  cncls2  23189  cncls  23190  cnntr  23191  cncnp  23196  cndis  23207  paste  23210  cmpfi  23324  conncompcld  23350  1stcfb  23361  1stccnp  23378  cldllycmp  23411  llycmpkgen2  23466  kgencn  23472  kgencn3  23474  dfac14lem  23533  txdis1cn  23551  hausdiag  23561  txkgen  23568  qtopval2  23612  basqtop  23627  qtopcld  23629  qtopeu  23632  qtoprest  23633  imastopn  23636  hmeontr  23685  hmeoimaf1o  23686  cmphaushmeo  23716  ordthmeolem  23717  elfm3  23866  rnelfmlem  23868  rnelfm  23869  alexsubALTlem4  23966  cldsubg  24027  tgpconncompeqg  24028  tgpconncomp  24029  qustgpopn  24036  qustgplem  24037  tsmsf1o  24061  ucncn  24200  imasf1oxms  24405  blcld  24421  metustfbas  24473  cfilucfil  24475  metuel2  24481  icchmeo  24866  icchmeoOLD  24867  relcmpcmet  25246  minveclem4a  25358  nulmbl2  25465  icombl  25493  ioombl  25494  uniiccdif  25507  volivth  25536  mbfres2  25574  itg1addlem5  25629  itgsplitioo  25767  dvcobr  25877  dvcobrOLD  25878  dvcnvlem  25908  lhop1lem  25946  lhop  25949  dvcnvrelem2  25951  uc1pval  26073  mon1pval  26075  vieta1lem2  26247  basellem5  27023  onnolt  28204  f1otrg  28850  axlowdimlem13  28934  axcontlem10  28953  uhgrspansubgr  29271  vtxdun  29462  pthdlem1  29746  eucrct2eupth  30227  ssmd1  32293  mdslj2i  32302  atcvat4i  32379  imadifxp  32583  nfpconfp  32616  2ndresdju  32633  ofpreima  32649  ofpreima2  32650  fsuppcurry1  32711  fsuppcurry2  32712  indpreima  32853  indf1ofs  32854  ccatws1f1olast  32940  gsumpart  33044  symgcom  33059  symgcom2  33060  pmtrcnel  33065  cycpmfvlem  33088  cycpmfv3  33091  elrgspnsubrunlem2  33222  elrspunidl  33400  idlinsubrg  33403  esplymhp  33608  fldextrspunlsp  33708  qtophaus  33870  reff  33873  locfinreflem  33874  zarcmplem  33915  hauseqcn  33932  oms0  34331  eulerpartlemv  34398  eulerpartlemb  34402  eulerpartlemr  34408  eulerpartlemgs2  34414  eulerpartlemn  34415  ballotlemro  34557  bnj1253  35050  bnj1280  35053  pthhashvtx  35193  acycgr0v  35213  prclisacycgr  35216  subfacp1lem3  35247  cvmscld  35338  cvmsss2  35339  cvmliftmolem1  35346  cvmliftlem7  35356  cvmlift2lem9  35376  cvmlift3lem7  35390  fnessref  36422  tailf  36440  poimirlem3  37683  mbfresfi  37726  cnambfre  37728  itg2addnclem2  37732  mettrifi  37817  ismtyres  37868  isdrngo2  38018  press  38531  diaintclN  41177  dibintclN  41286  dihintcl  41463  dochocss  41485  mapdunirnN  41769  pw2f1ocnv  43154  wessf1ornlem  45306  monoord2xrv  45605  itgcoscmulx  46091  ibliooicc  46093  stoweidlem11  46133  stoweidlem34  46156  fourierdlem48  46276  fourierdlem49  46277  fourierdlem74  46302  uniimaprimaeqfv  47506  elsetpreimafvssdm  47510  fdivmptf  48666  refdivmptf  48667  iscnrm3llem2  49074  imaidfu  49235