Theorem sseqtrid 3992

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  sseqtrrid  3993  iunxdif3  5062  fssdm  6710  fndmdif  7017  fneqeql2  7022  fconst4  7191  isofrlem  7318  fvmptopab  7446  f1opw2  7647  fparlem3  8096  fparlem4  8097  fnwelem  8113  fsuppeq  8157  fsuppeqg  8158  ecss  8725  pw2f1olem  9050  fopwdom  9054  ssenen  9121  ssfiALT  9144  fiint  9284  fiintOLD  9285  f1opwfi  9314  kmlem5  10115  enfin2i  10281  fpwwe2lem5  10595  fpwwe2lem8  10598  tskuni  10743  monoord2  14005  seqz  14022  cshimadifsn0  14803  binom1dif  15806  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  bitsres  16450  prdshom  17437  imasless  17510  cntzval  19260  f1omvdmvd  19380  f1omvdconj  19383  pmtrfb  19402  symggen  19407  symggen2  19408  psgnunilem1  19430  gsumzaddlem  19858  rngcbas  20537  ringcbas  20566  isdrngd  20681  isdrngdOLD  20683  lspextmo  20970  znleval  21471  freshmansdream  21491  ordtcld1  23091  ordtcld2  23092  cnpnei  23158  cnntri  23165  cncls2  23167  cncls  23168  cnntr  23169  cncnp  23174  cndis  23185  paste  23188  cmpfi  23302  conncompcld  23328  1stcfb  23339  1stccnp  23356  cldllycmp  23389  llycmpkgen2  23444  kgencn  23450  kgencn3  23452  dfac14lem  23511  txdis1cn  23529  hausdiag  23539  txkgen  23546  qtopval2  23590  basqtop  23605  qtopcld  23607  qtopeu  23610  qtoprest  23611  imastopn  23614  hmeontr  23663  hmeoimaf1o  23664  cmphaushmeo  23694  ordthmeolem  23695  elfm3  23844  rnelfmlem  23846  rnelfm  23847  alexsubALTlem4  23944  cldsubg  24005  tgpconncompeqg  24006  tgpconncomp  24007  qustgpopn  24014  qustgplem  24015  tsmsf1o  24039  ucncn  24179  imasf1oxms  24384  blcld  24400  metustfbas  24452  cfilucfil  24454  metuel2  24460  icchmeo  24845  icchmeoOLD  24846  relcmpcmet  25225  minveclem4a  25337  nulmbl2  25444  icombl  25472  ioombl  25473  uniiccdif  25486  volivth  25515  mbfres2  25553  itg1addlem5  25608  itgsplitioo  25746  dvcobr  25856  dvcobrOLD  25857  dvcnvlem  25887  lhop1lem  25925  lhop  25928  dvcnvrelem2  25930  uc1pval  26052  mon1pval  26054  vieta1lem2  26226  basellem5  27002  onnolt  28174  f1otrg  28805  axlowdimlem13  28888  axcontlem10  28907  uhgrspansubgr  29225  vtxdun  29416  pthdlem1  29703  eucrct2eupth  30181  ssmd1  32247  mdslj2i  32256  atcvat4i  32333  imadifxp  32537  nfpconfp  32563  2ndresdju  32580  ofpreima  32596  ofpreima2  32597  fsuppcurry1  32655  fsuppcurry2  32656  indpreima  32795  indf1ofs  32796  ccatws1f1olast  32881  gsumpart  33004  symgcom  33047  symgcom2  33048  pmtrcnel  33053  cycpmfvlem  33076  cycpmfv3  33079  elrgspnsubrunlem2  33206  elrspunidl  33406  idlinsubrg  33409  fldextrspunlsp  33676  qtophaus  33833  reff  33836  locfinreflem  33837  zarcmplem  33878  hauseqcn  33895  oms0  34295  eulerpartlemv  34362  eulerpartlemb  34366  eulerpartlemr  34372  eulerpartlemgs2  34378  eulerpartlemn  34379  ballotlemro  34521  bnj1253  35014  bnj1280  35017  pthhashvtx  35122  acycgr0v  35142  prclisacycgr  35145  subfacp1lem3  35176  cvmscld  35267  cvmsss2  35268  cvmliftmolem1  35275  cvmliftlem7  35285  cvmlift2lem9  35305  cvmlift3lem7  35319  fnessref  36352  tailf  36370  poimirlem3  37624  mbfresfi  37667  cnambfre  37669  itg2addnclem2  37673  mettrifi  37758  ismtyres  37809  isdrngo2  37959  diaintclN  41059  dibintclN  41168  dihintcl  41345  dochocss  41367  mapdunirnN  41651  pw2f1ocnv  43033  wessf1ornlem  45186  monoord2xrv  45486  itgcoscmulx  45974  ibliooicc  45976  stoweidlem11  46016  stoweidlem34  46039  fourierdlem48  46159  fourierdlem49  46160  fourierdlem74  46185  uniimaprimaeqfv  47387  elsetpreimafvssdm  47391  fdivmptf  48534  refdivmptf  48535  iscnrm3llem2  48942  imaidfu  49103