Theorem sseqtrid 3950

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseqtrrid  3951  iunxdif3  5054  fssdm  6730  fndmdif  7042  fneqeql2  7047  fconst4  7221  isofrlem  7349  fvmptopab  7476  f1opw2  7677  fparlem3  8128  fparlem4  8129  fnwelem  8146  fsuppeq  8196  fsuppeqg  8197  ecss  8773  pw2f1olem  9104  fopwdom  9108  ssenen  9174  ssfiALT  9193  fiint  9322  f1opwfi  9349  kmlem5  10237  enfin2i  10403  fpwwe2lem5  10724  fpwwe2lem8  10727  tskuni  10872  monoord2  14180  seqz  14197  cshimadifsn0  14986  binom1dif  16008  bpolycl  16224  bpolysum  16225  bpolydiflem  16226  bitsres  16649  prdshom  17644  imasless  17718  cntzval  19541  f1omvdmvd  19663  f1omvdconj  19666  pmtrfb  19685  symggen  19690  symggen2  19691  psgnunilem1  19713  gsumzaddlem  20141  rngcbas  20879  ringcbas  20908  isdrngd  21028  isdrngdOLD  21030  lspextmo  21337  znleval  21866  freshmansdream  21886  ordtcld1  23521  ordtcld2  23522  cnpnei  23588  cnntri  23595  cncls2  23597  cncls  23598  cnntr  23599  cncnp  23604  cndis  23615  paste  23618  cmpfi  23732  conncompcld  23758  1stcfb  23769  1stccnp  23787  cldllycmp  23820  llycmpkgen2  23875  kgencn  23881  kgencn3  23883  dfac14lem  23942  txdis1cn  23960  hausdiag  23970  txkgen  23977  qtopval2  24021  basqtop  24036  qtopcld  24038  qtopeu  24041  qtoprest  24042  imastopn  24045  hmeontr  24094  hmeoimaf1o  24095  cmphaushmeo  24125  ordthmeolem  24126  elfm3  24275  rnelfmlem  24277  rnelfm  24278  alexsubALTlem4  24375  cldsubg  24436  tgpconncompeqg  24437  tgpconncomp  24438  qustgpopn  24445  qustgplem  24446  tsmsf1o  24470  ucncn  24609  imasf1oxms  24814  blcld  24830  metustfbas  24882  cfilucfil  24884  metuel2  24890  icchmeo  25268  relcmpcmet  25645  minveclem4a  25757  nulmbl2  25863  icombl  25891  ioombl  25892  uniiccdif  25905  volivth  25934  mbfres2  25972  itg1addlem5  26027  itgsplitioo  26164  dvcobr  26272  dvcnvlem  26302  lhop1lem  26339  lhop  26342  dvcnvrelem2  26344  uc1pval  26464  mon1pval  26466  vieta1lem2  26640  basellem5  27418  onnolt  28658  f1otrg  29454  axlowdimlem13  29538  axcontlem10  29557  uhgrspansubgr  29878  vtxdun  30068  pthhashvtx  30321  pthdlem1  30358  eucrct2eupth  30852  ssmd1  32919  mdslj2i  32928  atcvat4i  33005  imadifxp  33243  nfpconfp  33274  2ndresdju  33291  ofpreima  33307  ofpreima2  33308  fsuppcurry1  33363  fsuppcurry2  33364  indpreima  33479  indf1ofs  33480  ccatws1f1olast  33562  gsumpart  33671  symgcom  33691  symgcom2  33692  pmtrcnel  33697  cycpmfvlem  33720  cycpmfv3  33723  elrgspnsubrunlem2  33856  elrspunidl  34025  idlinsubrg  34028  esplymhp  34247  esplyfval1  34252  esplyfvaln  34253  fldextrspunlsp  34353  qtophaus  34515  locfinreflem  34519  zarcmplem  34560  hauseqcn  34577  oms0  34976  eulerpartlemv  35043  eulerpartlemb  35047  eulerpartlemr  35053  eulerpartlemgs2  35059  eulerpartlemn  35060  ballotlemro  35202  bnj1253  35694  bnj1280  35697  onvfowev  35970  acycgr0v  35990  prclisacycgr  35993  subfacp1lem3  36034  cvmscld  36125  cvmsss2  36126  cvmliftmolem1  36133  cvmliftlem7  36143  cvmlift2lem9  36163  cvmlift3lem7  36177  fnessref  37238  tailf  37256  poimirlem3  38635  mbfresfi  38678  cnambfre  38680  itg2addnclem2  38684  mettrifi  38785  ismtyres  38836  isdrngo2  38986  press  39525  diaintclN  42209  dibintclN  42318  dihintcl  42495  dochocss  42517  mapdunirnN  42801  pw2f1ocnv  44138  wessf1ornlem  46294  monoord2xrv  46587  itgcoscmulx  47073  ibliooicc  47075  stoweidlem11  47115  stoweidlem34  47138  fourierdlem48  47258  fourierdlem49  47259  fourierdlem74  47284  tmachlem-agreeprod  48041  uniimaprimaeqfv  48558  elsetpreimafvssdm  48562  fdivmptf  49747  refdivmptf  49748  iscnrm3llem2  50158  imaidfu  50320