Theorem sseqtrid 3977

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  sseqtrrid  3978  iunxdif3  5043  fssdm  6670  fndmdif  6975  fneqeql2  6980  fconst4  7148  isofrlem  7274  fvmptopab  7401  f1opw2  7601  fparlem3  8044  fparlem4  8045  fnwelem  8061  fsuppeq  8105  fsuppeqg  8106  ecss  8673  pw2f1olem  8994  fopwdom  8998  ssenen  9064  ssfiALT  9083  fiint  9211  f1opwfi  9240  kmlem5  10043  enfin2i  10209  fpwwe2lem5  10523  fpwwe2lem8  10526  tskuni  10671  monoord2  13937  seqz  13954  cshimadifsn0  14734  binom1dif  15737  bpolycl  15956  bpolysum  15957  bpolydiflem  15958  bitsres  16381  prdshom  17368  imasless  17441  cntzval  19231  f1omvdmvd  19353  f1omvdconj  19356  pmtrfb  19375  symggen  19380  symggen2  19381  psgnunilem1  19403  gsumzaddlem  19831  rngcbas  20534  ringcbas  20563  isdrngd  20678  isdrngdOLD  20680  lspextmo  20988  znleval  21489  freshmansdream  21509  ordtcld1  23110  ordtcld2  23111  cnpnei  23177  cnntri  23184  cncls2  23186  cncls  23187  cnntr  23188  cncnp  23193  cndis  23204  paste  23207  cmpfi  23321  conncompcld  23347  1stcfb  23358  1stccnp  23375  cldllycmp  23408  llycmpkgen2  23463  kgencn  23469  kgencn3  23471  dfac14lem  23530  txdis1cn  23548  hausdiag  23558  txkgen  23565  qtopval2  23609  basqtop  23624  qtopcld  23626  qtopeu  23629  qtoprest  23630  imastopn  23633  hmeontr  23682  hmeoimaf1o  23683  cmphaushmeo  23713  ordthmeolem  23714  elfm3  23863  rnelfmlem  23865  rnelfm  23866  alexsubALTlem4  23963  cldsubg  24024  tgpconncompeqg  24025  tgpconncomp  24026  qustgpopn  24033  qustgplem  24034  tsmsf1o  24058  ucncn  24197  imasf1oxms  24402  blcld  24418  metustfbas  24470  cfilucfil  24472  metuel2  24478  icchmeo  24863  icchmeoOLD  24864  relcmpcmet  25243  minveclem4a  25355  nulmbl2  25462  icombl  25490  ioombl  25491  uniiccdif  25504  volivth  25533  mbfres2  25571  itg1addlem5  25626  itgsplitioo  25764  dvcobr  25874  dvcobrOLD  25875  dvcnvlem  25905  lhop1lem  25943  lhop  25946  dvcnvrelem2  25948  uc1pval  26070  mon1pval  26072  vieta1lem2  26244  basellem5  27020  onnolt  28201  f1otrg  28847  axlowdimlem13  28930  axcontlem10  28949  uhgrspansubgr  29267  vtxdun  29458  pthdlem1  29742  eucrct2eupth  30220  ssmd1  32286  mdslj2i  32295  atcvat4i  32372  imadifxp  32576  nfpconfp  32609  2ndresdju  32626  ofpreima  32642  ofpreima2  32643  fsuppcurry1  32702  fsuppcurry2  32703  indpreima  32841  indf1ofs  32842  ccatws1f1olast  32928  gsumpart  33032  symgcom  33047  symgcom2  33048  pmtrcnel  33053  cycpmfvlem  33076  cycpmfv3  33079  elrgspnsubrunlem2  33210  elrspunidl  33388  idlinsubrg  33391  esplymhp  33584  fldextrspunlsp  33682  qtophaus  33844  reff  33847  locfinreflem  33848  zarcmplem  33889  hauseqcn  33906  oms0  34305  eulerpartlemv  34372  eulerpartlemb  34376  eulerpartlemr  34382  eulerpartlemgs2  34388  eulerpartlemn  34389  ballotlemro  34531  bnj1253  35024  bnj1280  35027  pthhashvtx  35160  acycgr0v  35180  prclisacycgr  35183  subfacp1lem3  35214  cvmscld  35305  cvmsss2  35306  cvmliftmolem1  35313  cvmliftlem7  35323  cvmlift2lem9  35343  cvmlift3lem7  35357  fnessref  36390  tailf  36408  poimirlem3  37662  mbfresfi  37705  cnambfre  37707  itg2addnclem2  37711  mettrifi  37796  ismtyres  37847  isdrngo2  37997  diaintclN  41096  dibintclN  41205  dihintcl  41382  dochocss  41404  mapdunirnN  41688  pw2f1ocnv  43069  wessf1ornlem  45221  monoord2xrv  45520  itgcoscmulx  46006  ibliooicc  46008  stoweidlem11  46048  stoweidlem34  46071  fourierdlem48  46191  fourierdlem49  46192  fourierdlem74  46217  uniimaprimaeqfv  47412  elsetpreimafvssdm  47416  fdivmptf  48572  refdivmptf  48573  iscnrm3llem2  48980  imaidfu  49141