Theorem sseqtrid 3980

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

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

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 2701

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

This theorem is referenced by:  sseqtrrid  3981  iunxdif3  5047  fssdm  6675  fndmdif  6980  fneqeql2  6985  fconst4  7154  isofrlem  7281  fvmptopab  7408  f1opw2  7608  fparlem3  8054  fparlem4  8055  fnwelem  8071  fsuppeq  8115  fsuppeqg  8116  ecss  8683  pw2f1olem  9005  fopwdom  9009  ssenen  9075  ssfiALT  9098  fiint  9235  fiintOLD  9236  f1opwfi  9265  kmlem5  10068  enfin2i  10234  fpwwe2lem5  10548  fpwwe2lem8  10551  tskuni  10696  monoord2  13958  seqz  13975  cshimadifsn0  14755  binom1dif  15758  bpolycl  15977  bpolysum  15978  bpolydiflem  15979  bitsres  16402  prdshom  17389  imasless  17462  cntzval  19218  f1omvdmvd  19340  f1omvdconj  19343  pmtrfb  19362  symggen  19367  symggen2  19368  psgnunilem1  19390  gsumzaddlem  19818  rngcbas  20524  ringcbas  20553  isdrngd  20668  isdrngdOLD  20670  lspextmo  20978  znleval  21479  freshmansdream  21499  ordtcld1  23100  ordtcld2  23101  cnpnei  23167  cnntri  23174  cncls2  23176  cncls  23177  cnntr  23178  cncnp  23183  cndis  23194  paste  23197  cmpfi  23311  conncompcld  23337  1stcfb  23348  1stccnp  23365  cldllycmp  23398  llycmpkgen2  23453  kgencn  23459  kgencn3  23461  dfac14lem  23520  txdis1cn  23538  hausdiag  23548  txkgen  23555  qtopval2  23599  basqtop  23614  qtopcld  23616  qtopeu  23619  qtoprest  23620  imastopn  23623  hmeontr  23672  hmeoimaf1o  23673  cmphaushmeo  23703  ordthmeolem  23704  elfm3  23853  rnelfmlem  23855  rnelfm  23856  alexsubALTlem4  23953  cldsubg  24014  tgpconncompeqg  24015  tgpconncomp  24016  qustgpopn  24023  qustgplem  24024  tsmsf1o  24048  ucncn  24188  imasf1oxms  24393  blcld  24409  metustfbas  24461  cfilucfil  24463  metuel2  24469  icchmeo  24854  icchmeoOLD  24855  relcmpcmet  25234  minveclem4a  25346  nulmbl2  25453  icombl  25481  ioombl  25482  uniiccdif  25495  volivth  25524  mbfres2  25562  itg1addlem5  25617  itgsplitioo  25755  dvcobr  25865  dvcobrOLD  25866  dvcnvlem  25896  lhop1lem  25934  lhop  25937  dvcnvrelem2  25939  uc1pval  26061  mon1pval  26063  vieta1lem2  26235  basellem5  27011  onnolt  28190  f1otrg  28834  axlowdimlem13  28917  axcontlem10  28936  uhgrspansubgr  29254  vtxdun  29445  pthdlem1  29729  eucrct2eupth  30207  ssmd1  32273  mdslj2i  32282  atcvat4i  32359  imadifxp  32563  nfpconfp  32589  2ndresdju  32606  ofpreima  32622  ofpreima2  32623  fsuppcurry1  32681  fsuppcurry2  32682  indpreima  32821  indf1ofs  32822  ccatws1f1olast  32907  gsumpart  33023  symgcom  33038  symgcom2  33039  pmtrcnel  33044  cycpmfvlem  33067  cycpmfv3  33070  elrgspnsubrunlem2  33198  elrspunidl  33375  idlinsubrg  33378  fldextrspunlsp  33645  qtophaus  33802  reff  33805  locfinreflem  33806  zarcmplem  33847  hauseqcn  33864  oms0  34264  eulerpartlemv  34331  eulerpartlemb  34335  eulerpartlemr  34341  eulerpartlemgs2  34347  eulerpartlemn  34348  ballotlemro  34490  bnj1253  34983  bnj1280  34986  pthhashvtx  35100  acycgr0v  35120  prclisacycgr  35123  subfacp1lem3  35154  cvmscld  35245  cvmsss2  35246  cvmliftmolem1  35253  cvmliftlem7  35263  cvmlift2lem9  35283  cvmlift3lem7  35297  fnessref  36330  tailf  36348  poimirlem3  37602  mbfresfi  37645  cnambfre  37647  itg2addnclem2  37651  mettrifi  37736  ismtyres  37787  isdrngo2  37937  diaintclN  41037  dibintclN  41146  dihintcl  41323  dochocss  41345  mapdunirnN  41629  pw2f1ocnv  43010  wessf1ornlem  45163  monoord2xrv  45463  itgcoscmulx  45951  ibliooicc  45953  stoweidlem11  45993  stoweidlem34  46016  fourierdlem48  46136  fourierdlem49  46137  fourierdlem74  46162  uniimaprimaeqfv  47367  elsetpreimafvssdm  47371  fdivmptf  48527  refdivmptf  48528  iscnrm3llem2  48935  imaidfu  49096