Theorem sseqtrid 4008

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3950

This theorem is referenced by:  sseqtrrid  4009  iunxdif3  5077  fssdm  6736  fndmdif  7043  fneqeql2  7048  fconst4  7217  isofrlem  7343  fvmptopab  7470  f1opw2  7671  fparlem3  8122  fparlem4  8123  fnwelem  8139  fsuppeq  8183  fsuppeqg  8184  ecss  8776  pw2f1olem  9099  fopwdom  9103  ssenen  9174  ssfiALT  9197  phplem2OLD  9238  fiint  9349  fiintOLD  9350  f1opwfi  9379  kmlem5  10178  enfin2i  10344  fpwwe2lem5  10658  fpwwe2lem8  10661  tskuni  10806  monoord2  14057  seqz  14074  cshimadifsn0  14852  binom1dif  15852  bpolycl  16071  bpolysum  16072  bpolydiflem  16073  bitsres  16493  prdshom  17488  imasless  17561  cntzval  19313  f1omvdmvd  19434  f1omvdconj  19437  pmtrfb  19456  symggen  19461  symggen2  19462  psgnunilem1  19484  gsumzaddlem  19912  rngcbas  20594  ringcbas  20623  isdrngd  20738  isdrngdOLD  20740  lspextmo  21028  znleval  21540  freshmansdream  21560  ordtcld1  23170  ordtcld2  23171  cnpnei  23237  cnntri  23244  cncls2  23246  cncls  23247  cnntr  23248  cncnp  23253  cndis  23264  paste  23267  cmpfi  23381  conncompcld  23407  1stcfb  23418  1stccnp  23435  cldllycmp  23468  llycmpkgen2  23523  kgencn  23529  kgencn3  23531  dfac14lem  23590  txdis1cn  23608  hausdiag  23618  txkgen  23625  qtopval2  23669  basqtop  23684  qtopcld  23686  qtopeu  23689  qtoprest  23690  imastopn  23693  hmeontr  23742  hmeoimaf1o  23743  cmphaushmeo  23773  ordthmeolem  23774  elfm3  23923  rnelfmlem  23925  rnelfm  23926  alexsubALTlem4  24023  cldsubg  24084  tgpconncompeqg  24085  tgpconncomp  24086  qustgpopn  24093  qustgplem  24094  tsmsf1o  24118  ucncn  24258  imasf1oxms  24465  blcld  24481  metustfbas  24533  cfilucfil  24535  metuel2  24541  icchmeo  24926  icchmeoOLD  24927  relcmpcmet  25307  minveclem4a  25419  nulmbl2  25526  icombl  25554  ioombl  25555  uniiccdif  25568  volivth  25597  mbfres2  25635  itg1addlem5  25690  itgsplitioo  25828  dvcobr  25938  dvcobrOLD  25939  dvcnvlem  25969  lhop1lem  26007  lhop  26010  dvcnvrelem2  26012  uc1pval  26134  mon1pval  26136  vieta1lem2  26308  basellem5  27083  f1otrg  28834  axlowdimlem13  28918  axcontlem10  28937  uhgrspansubgr  29255  vtxdun  29446  pthdlem1  29733  eucrct2eupth  30211  ssmd1  32277  mdslj2i  32286  atcvat4i  32363  imadifxp  32561  nfpconfp  32589  2ndresdju  32606  ofpreima  32622  ofpreima2  32623  fsuppcurry1  32683  fsuppcurry2  32684  indpreima  32797  indf1ofs  32798  ccatws1f1olast  32884  gsumpart  33006  symgcom  33049  symgcom2  33050  pmtrcnel  33055  cycpmfvlem  33078  cycpmfv3  33081  elrgspnsubrunlem2  33198  elrspunidl  33397  idlinsubrg  33400  fldextrspunlsp  33665  qtophaus  33776  reff  33779  locfinreflem  33780  zarcmplem  33821  hauseqcn  33838  oms0  34240  eulerpartlemv  34307  eulerpartlemb  34311  eulerpartlemr  34317  eulerpartlemgs2  34323  eulerpartlemn  34324  ballotlemro  34466  bnj1253  34972  bnj1280  34975  pthhashvtx  35074  acycgr0v  35094  prclisacycgr  35097  subfacp1lem3  35128  cvmscld  35219  cvmsss2  35220  cvmliftmolem1  35227  cvmliftlem7  35237  cvmlift2lem9  35257  cvmlift3lem7  35271  fnessref  36299  tailf  36317  poimirlem3  37571  mbfresfi  37614  cnambfre  37616  itg2addnclem2  37620  mettrifi  37705  ismtyres  37756  isdrngo2  37906  diaintclN  41001  dibintclN  41110  dihintcl  41287  dochocss  41309  mapdunirnN  41593  pw2f1ocnv  42994  wessf1ornlem  45135  monoord2xrv  45439  itgcoscmulx  45929  ibliooicc  45931  stoweidlem11  45971  stoweidlem34  45994  fourierdlem48  46114  fourierdlem49  46115  fourierdlem74  46140  uniimaprimaeqfv  47315  elsetpreimafvssdm  47319  fdivmptf  48408  refdivmptf  48409  iscnrm3llem2  48795