Theorem sseqtrid 4061

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseqtrrid  4062  iunxdif3  5118  fssdm  6766  fndmdif  7075  fneqeql2  7080  fconst4  7251  isofrlem  7376  fvmptopab  7504  f1opw2  7705  fparlem3  8155  fparlem4  8156  fnwelem  8172  fsuppeq  8216  fsuppeqg  8217  ecss  8811  pw2f1olem  9142  fopwdom  9146  ssenen  9217  ssfiALT  9241  phplem2OLD  9281  fiint  9394  fiintOLD  9395  f1opwfi  9426  kmlem5  10224  enfin2i  10390  fpwwe2lem5  10704  fpwwe2lem8  10707  tskuni  10852  monoord2  14084  seqz  14101  cshimadifsn0  14879  binom1dif  15881  bpolycl  16100  bpolysum  16101  bpolydiflem  16102  bitsres  16519  prdshom  17527  imasless  17600  cntzval  19361  f1omvdmvd  19485  f1omvdconj  19488  pmtrfb  19507  symggen  19512  symggen2  19513  psgnunilem1  19535  gsumzaddlem  19963  rngcbas  20643  ringcbas  20672  isdrngd  20787  isdrngdOLD  20789  lspextmo  21078  znleval  21596  freshmansdream  21616  ordtcld1  23226  ordtcld2  23227  cnpnei  23293  cnntri  23300  cncls2  23302  cncls  23303  cnntr  23304  cncnp  23309  cndis  23320  paste  23323  cmpfi  23437  conncompcld  23463  1stcfb  23474  1stccnp  23491  cldllycmp  23524  llycmpkgen2  23579  kgencn  23585  kgencn3  23587  dfac14lem  23646  txdis1cn  23664  hausdiag  23674  txkgen  23681  qtopval2  23725  basqtop  23740  qtopcld  23742  qtopeu  23745  qtoprest  23746  imastopn  23749  hmeontr  23798  hmeoimaf1o  23799  cmphaushmeo  23829  ordthmeolem  23830  elfm3  23979  rnelfmlem  23981  rnelfm  23982  alexsubALTlem4  24079  cldsubg  24140  tgpconncompeqg  24141  tgpconncomp  24142  qustgpopn  24149  qustgplem  24150  tsmsf1o  24174  ucncn  24315  imasf1oxms  24523  blcld  24539  metustfbas  24591  cfilucfil  24593  metuel2  24599  icchmeo  24990  icchmeoOLD  24991  relcmpcmet  25371  minveclem4a  25483  nulmbl2  25590  icombl  25618  ioombl  25619  uniiccdif  25632  volivth  25661  mbfres2  25699  itg1addlem5  25755  itgsplitioo  25893  dvcobr  26003  dvcobrOLD  26004  dvcnvlem  26034  lhop1lem  26072  lhop  26075  dvcnvrelem2  26077  uc1pval  26199  mon1pval  26201  vieta1lem2  26371  basellem5  27146  f1otrg  28897  axlowdimlem13  28987  axcontlem10  29006  uhgrspansubgr  29326  vtxdun  29517  pthdlem1  29802  eucrct2eupth  30277  ssmd1  32343  mdslj2i  32352  atcvat4i  32429  imadifxp  32623  nfpconfp  32651  2ndresdju  32667  ofpreima  32683  ofpreima2  32684  fsuppcurry1  32739  fsuppcurry2  32740  ccatws1f1olast  32919  gsumpart  33038  symgcom  33076  symgcom2  33077  pmtrcnel  33082  cycpmfvlem  33105  cycpmfv3  33108  elrspunidl  33421  idlinsubrg  33424  qtophaus  33782  reff  33785  locfinreflem  33786  zarcmplem  33827  hauseqcn  33844  indpreima  33989  indf1ofs  33990  oms0  34262  eulerpartlemv  34329  eulerpartlemb  34333  eulerpartlemr  34339  eulerpartlemgs2  34345  eulerpartlemn  34346  ballotlemro  34487  bnj1253  34993  bnj1280  34996  pthhashvtx  35095  acycgr0v  35116  prclisacycgr  35119  subfacp1lem3  35150  cvmscld  35241  cvmsss2  35242  cvmliftmolem1  35249  cvmliftlem7  35259  cvmlift2lem9  35279  cvmlift3lem7  35293  fnessref  36323  tailf  36341  poimirlem3  37583  mbfresfi  37626  cnambfre  37628  itg2addnclem2  37632  mettrifi  37717  ismtyres  37768  isdrngo2  37918  diaintclN  41015  dibintclN  41124  dihintcl  41301  dochocss  41323  mapdunirnN  41607  pw2f1ocnv  42994  wessf1ornlem  45092  monoord2xrv  45399  itgcoscmulx  45890  ibliooicc  45892  stoweidlem11  45932  stoweidlem34  45955  fourierdlem48  46075  fourierdlem49  46076  fourierdlem74  46101  uniimaprimaeqfv  47256  elsetpreimafvssdm  47260  fdivmptf  48275  refdivmptf  48276  iscnrm3llem2  48630