Theorem sseqtrid 3978

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

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

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 2709

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

This theorem is referenced by:  sseqtrrid  3979  iunxdif3  5052  fssdm  6689  fndmdif  6996  fneqeql2  7001  fconst4  7170  isofrlem  7296  fvmptopab  7423  f1opw2  7623  fparlem3  8066  fparlem4  8067  fnwelem  8083  fsuppeq  8127  fsuppeqg  8128  ecss  8697  pw2f1olem  9021  fopwdom  9025  ssenen  9091  ssfiALT  9110  fiint  9239  f1opwfi  9268  kmlem5  10077  enfin2i  10243  fpwwe2lem5  10558  fpwwe2lem8  10561  tskuni  10706  monoord2  13968  seqz  13985  cshimadifsn0  14765  binom1dif  15768  bpolycl  15987  bpolysum  15988  bpolydiflem  15989  bitsres  16412  prdshom  17399  imasless  17473  cntzval  19262  f1omvdmvd  19384  f1omvdconj  19387  pmtrfb  19406  symggen  19411  symggen2  19412  psgnunilem1  19434  gsumzaddlem  19862  rngcbas  20566  ringcbas  20595  isdrngd  20710  isdrngdOLD  20712  lspextmo  21020  znleval  21521  freshmansdream  21541  ordtcld1  23153  ordtcld2  23154  cnpnei  23220  cnntri  23227  cncls2  23229  cncls  23230  cnntr  23231  cncnp  23236  cndis  23247  paste  23250  cmpfi  23364  conncompcld  23390  1stcfb  23401  1stccnp  23418  cldllycmp  23451  llycmpkgen2  23506  kgencn  23512  kgencn3  23514  dfac14lem  23573  txdis1cn  23591  hausdiag  23601  txkgen  23608  qtopval2  23652  basqtop  23667  qtopcld  23669  qtopeu  23672  qtoprest  23673  imastopn  23676  hmeontr  23725  hmeoimaf1o  23726  cmphaushmeo  23756  ordthmeolem  23757  elfm3  23906  rnelfmlem  23908  rnelfm  23909  alexsubALTlem4  24006  cldsubg  24067  tgpconncompeqg  24068  tgpconncomp  24069  qustgpopn  24076  qustgplem  24077  tsmsf1o  24101  ucncn  24240  imasf1oxms  24445  blcld  24461  metustfbas  24513  cfilucfil  24515  metuel2  24521  icchmeo  24906  icchmeoOLD  24907  relcmpcmet  25286  minveclem4a  25398  nulmbl2  25505  icombl  25533  ioombl  25534  uniiccdif  25547  volivth  25576  mbfres2  25614  itg1addlem5  25669  itgsplitioo  25807  dvcobr  25917  dvcobrOLD  25918  dvcnvlem  25948  lhop1lem  25986  lhop  25989  dvcnvrelem2  25991  uc1pval  26113  mon1pval  26115  vieta1lem2  26287  basellem5  27063  onnolt  28274  f1otrg  28955  axlowdimlem13  29039  axcontlem10  29058  uhgrspansubgr  29376  vtxdun  29567  pthdlem1  29851  eucrct2eupth  30332  ssmd1  32398  mdslj2i  32407  atcvat4i  32484  imadifxp  32687  nfpconfp  32721  2ndresdju  32738  ofpreima  32754  ofpreima2  32755  fsuppcurry1  32813  fsuppcurry2  32814  indpreima  32957  indf1ofs  32958  ccatws1f1olast  33044  gsumpart  33156  symgcom  33176  symgcom2  33177  pmtrcnel  33182  cycpmfvlem  33205  cycpmfv3  33208  elrgspnsubrunlem2  33341  elrspunidl  33520  idlinsubrg  33523  esplymhp  33744  esplyfval1  33749  esplyfvaln  33750  fldextrspunlsp  33851  qtophaus  34013  reff  34016  locfinreflem  34017  zarcmplem  34058  hauseqcn  34075  oms0  34474  eulerpartlemv  34541  eulerpartlemb  34545  eulerpartlemr  34551  eulerpartlemgs2  34557  eulerpartlemn  34558  ballotlemro  34700  bnj1253  35192  bnj1280  35195  pthhashvtx  35341  acycgr0v  35361  prclisacycgr  35364  subfacp1lem3  35395  cvmscld  35486  cvmsss2  35487  cvmliftmolem1  35494  cvmliftlem7  35504  cvmlift2lem9  35524  cvmlift3lem7  35538  fnessref  36570  tailf  36588  poimirlem3  37868  mbfresfi  37911  cnambfre  37913  itg2addnclem2  37917  mettrifi  38002  ismtyres  38053  isdrngo2  38203  press  38744  diaintclN  41428  dibintclN  41537  dihintcl  41714  dochocss  41736  mapdunirnN  42020  pw2f1ocnv  43388  wessf1ornlem  45538  monoord2xrv  45835  itgcoscmulx  46321  ibliooicc  46323  stoweidlem11  46363  stoweidlem34  46386  fourierdlem48  46506  fourierdlem49  46507  fourierdlem74  46532  uniimaprimaeqfv  47736  elsetpreimafvssdm  47740  fdivmptf  48895  refdivmptf  48896  iscnrm3llem2  49303  imaidfu  49463