Theorem sseqtrid 4031

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3952  df-ss 3962

This theorem is referenced by:  sseqtrrid  4032  iunxdif3  5092  fssdm  6725  fndmdif  7029  fneqeql2  7034  fconst4  7201  isofrlem  7322  fvmptopab  7448  f1opw2  7645  fparlem3  8084  fparlem4  8085  fnwelem  8101  fsuppeq  8144  fsuppeqg  8145  ecss  8734  pw2f1olem  9061  fopwdom  9065  ssenen  9136  ssfiALT  9159  phplem2OLD  9203  fiint  9309  f1opwfi  9341  kmlem5  10133  enfin2i  10300  fpwwe2lem5  10614  fpwwe2lem8  10617  tskuni  10762  monoord2  13983  seqz  14000  cshimadifsn0  14765  binom1dif  15763  bpolycl  15980  bpolysum  15981  bpolydiflem  15982  bitsres  16398  prdshom  17397  imasless  17470  cntzval  19153  f1omvdmvd  19277  f1omvdconj  19280  pmtrfb  19299  symggen  19304  symggen2  19305  psgnunilem1  19327  gsumzaddlem  19750  isdrngd  20299  isdrngdOLD  20301  lspextmo  20618  znleval  21045  ordtcld1  22632  ordtcld2  22633  cnpnei  22699  cnntri  22706  cncls2  22708  cncls  22709  cnntr  22710  cncnp  22715  cndis  22726  paste  22729  cmpfi  22843  conncompcld  22869  1stcfb  22880  1stccnp  22897  cldllycmp  22930  llycmpkgen2  22985  kgencn  22991  kgencn3  22993  dfac14lem  23052  txdis1cn  23070  hausdiag  23080  txkgen  23087  qtopval2  23131  basqtop  23146  qtopcld  23148  qtopeu  23151  qtoprest  23152  imastopn  23155  hmeontr  23204  hmeoimaf1o  23205  cmphaushmeo  23235  ordthmeolem  23236  elfm3  23385  rnelfmlem  23387  rnelfm  23388  alexsubALTlem4  23485  cldsubg  23546  tgpconncompeqg  23547  tgpconncomp  23548  qustgpopn  23555  qustgplem  23556  tsmsf1o  23580  ucncn  23721  imasf1oxms  23929  blcld  23945  metustfbas  23997  cfilucfil  23999  metuel2  24005  icchmeo  24388  relcmpcmet  24766  minveclem4a  24878  nulmbl2  24984  icombl  25012  ioombl  25013  uniiccdif  25026  volivth  25055  mbfres2  25093  itg1addlem5  25149  itgsplitioo  25286  dvcobr  25394  dvcnvlem  25424  lhop1lem  25461  lhop  25464  dvcnvrelem2  25466  uc1pval  25588  mon1pval  25590  vieta1lem2  25755  basellem5  26518  f1otrg  28051  axlowdimlem13  28141  axcontlem10  28160  uhgrspansubgr  28477  vtxdun  28667  pthdlem1  28952  eucrct2eupth  29427  ssmd1  31491  mdslj2i  31500  atcvat4i  31577  imadifxp  31761  nfpconfp  31788  2ndresdju  31807  ofpreima  31823  ofpreima2  31824  fsuppcurry1  31885  fsuppcurry2  31886  gsumpart  32142  symgcom  32179  symgcom2  32180  pmtrcnel  32185  cycpmfvlem  32206  cycpmfv3  32209  freshmansdream  32313  elrspunidl  32461  idlinsubrg  32464  qtophaus  32711  reff  32714  locfinreflem  32715  zarcmplem  32756  hauseqcn  32773  indpreima  32918  indf1ofs  32919  oms0  33191  eulerpartlemv  33258  eulerpartlemb  33262  eulerpartlemr  33268  eulerpartlemgs2  33274  eulerpartlemn  33275  ballotlemro  33416  bnj1253  33923  bnj1280  33926  pthhashvtx  34013  acycgr0v  34034  prclisacycgr  34037  subfacp1lem3  34068  cvmscld  34159  cvmsss2  34160  cvmliftmolem1  34167  cvmliftlem7  34177  cvmlift2lem9  34197  cvmlift3lem7  34211  fnessref  35110  tailf  35128  poimirlem3  36359  mbfresfi  36402  cnambfre  36404  itg2addnclem2  36408  mettrifi  36494  ismtyres  36545  isdrngo2  36695  diaintclN  39798  dibintclN  39907  dihintcl  40084  dochocss  40106  mapdunirnN  40390  pw2f1ocnv  41611  wessf1ornlem  43717  monoord2xrv  44031  itgcoscmulx  44522  ibliooicc  44524  stoweidlem11  44564  stoweidlem34  44587  fourierdlem48  44707  fourierdlem49  44708  fourierdlem74  44733  uniimaprimaeqfv  45886  elsetpreimafvssdm  45890  rngcbas  46575  ringcbas  46621  fdivmptf  46939  refdivmptf  46940  iscnrm3llem2  47295