Theorem sseqtrid 3982

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  sseqtrrid  3983  iunxdif3  5066  fssdm  6732  fndmdif  7044  fneqeql2  7049  fconst4  7219  isofrlem  7349  fvmptopab  7478  f1opw2  7678  fparlem3  8118  fparlem4  8119  fnwelem  8136  fsuppeq  8180  fsuppeqg  8181  ecss  8755  pw2f1olem  9079  fopwdom  9083  ssenen  9149  ssfiALT  9168  fiint  9296  f1opwfi  9323  kmlem5  10157  enfin2i  10323  fpwwe2lem5  10638  fpwwe2lem8  10641  tskuni  10786  monoord2  14089  seqz  14106  cshimadifsn0  14893  binom1dif  15913  bpolycl  16131  bpolysum  16132  bpolydiflem  16133  bitsres  16556  prdshom  17545  imasless  17619  cntzval  19422  f1omvdmvd  19544  f1omvdconj  19547  pmtrfb  19566  symggen  19571  symggen2  19572  psgnunilem1  19594  gsumzaddlem  20022  rngcbas  20757  ringcbas  20786  isdrngd  20905  isdrngdOLD  20907  lspextmo  21214  znleval  21741  freshmansdream  21761  ordtcld1  23391  ordtcld2  23392  cnpnei  23458  cnntri  23465  cncls2  23467  cncls  23468  cnntr  23469  cncnp  23474  cndis  23485  paste  23488  cmpfi  23602  conncompcld  23628  1stcfb  23639  1stccnp  23656  cldllycmp  23689  llycmpkgen2  23744  kgencn  23750  kgencn3  23752  dfac14lem  23811  txdis1cn  23829  hausdiag  23839  txkgen  23846  qtopval2  23890  basqtop  23905  qtopcld  23907  qtopeu  23910  qtoprest  23911  imastopn  23914  hmeontr  23963  hmeoimaf1o  23964  cmphaushmeo  23994  ordthmeolem  23995  elfm3  24144  rnelfmlem  24146  rnelfm  24147  alexsubALTlem4  24244  cldsubg  24305  tgpconncompeqg  24306  tgpconncomp  24307  qustgpopn  24314  qustgplem  24315  tsmsf1o  24339  ucncn  24478  imasf1oxms  24683  blcld  24699  metustfbas  24751  cfilucfil  24753  metuel2  24759  icchmeo  25137  relcmpcmet  25514  minveclem4a  25626  nulmbl2  25732  icombl  25760  ioombl  25761  uniiccdif  25774  volivth  25803  mbfres2  25841  itg1addlem5  25896  itgsplitioo  26034  dvcobr  26142  dvcnvlem  26172  lhop1lem  26209  lhop  26212  dvcnvrelem2  26214  uc1pval  26334  mon1pval  26336  vieta1lem2  26509  basellem5  27286  onnolt  28496  f1otrg  29257  axlowdimlem13  29341  axcontlem10  29360  uhgrspansubgr  29678  vtxdun  29868  pthdlem1  30152  eucrct2eupth  30633  ssmd1  32700  mdslj2i  32709  atcvat4i  32786  imadifxp  32983  nfpconfp  33014  2ndresdju  33031  ofpreima  33047  ofpreima2  33048  fsuppcurry1  33106  fsuppcurry2  33107  indpreima  33222  indf1ofs  33223  ccatws1f1olast  33305  gsumpart  33414  symgcom  33434  symgcom2  33435  pmtrcnel  33440  cycpmfvlem  33463  cycpmfv3  33466  elrgspnsubrunlem2  33599  elrspunidl  33767  idlinsubrg  33770  esplymhp  33989  esplyfval1  33994  esplyfvaln  33995  fldextrspunlsp  34095  qtophaus  34257  reff  34260  locfinreflem  34261  zarcmplem  34302  hauseqcn  34319  oms0  34719  eulerpartlemv  34786  eulerpartlemb  34790  eulerpartlemr  34796  eulerpartlemgs2  34802  eulerpartlemn  34803  ballotlemro  34945  bnj1253  35437  bnj1280  35440  onvfowev  35624  pthhashvtx  35641  acycgr0v  35661  prclisacycgr  35664  subfacp1lem3  35695  cvmscld  35786  cvmsss2  35787  cvmliftmolem1  35794  cvmliftlem7  35804  cvmlift2lem9  35824  cvmlift3lem7  35838  fnessref  36909  tailf  36927  poimirlem3  38315  mbfresfi  38358  cnambfre  38360  itg2addnclem2  38364  mettrifi  38449  ismtyres  38500  isdrngo2  38650  press  39189  diaintclN  41873  dibintclN  41982  dihintcl  42159  dochocss  42181  mapdunirnN  42465  pw2f1ocnv  43805  wessf1ornlem  45944  monoord2xrv  46238  itgcoscmulx  46724  ibliooicc  46726  stoweidlem11  46766  stoweidlem34  46789  fourierdlem48  46909  fourierdlem49  46910  fourierdlem74  46935  uniimaprimaeqfv  48172  elsetpreimafvssdm  48176  fdivmptf  49362  refdivmptf  49363  iscnrm3llem2  49769  imaidfu  49929