Theorem sseqtrid 3976

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

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

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 2155  ax-ext 2734

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

This theorem is used by:  sseqtrrid  3977  iunxdif3  5059  fssdm  6726  fndmdif  7038  fneqeql2  7043  fconst4  7217  isofrlem  7345  fvmptopab  7472  f1opw2  7673  fparlem3  8115  fparlem4  8116  fnwelem  8133  fsuppeq  8177  fsuppeqg  8178  ecss  8752  pw2f1olem  9083  fopwdom  9087  ssenen  9153  ssfiALT  9172  fiint  9300  f1opwfi  9327  kmlem5  10161  enfin2i  10327  fpwwe2lem5  10648  fpwwe2lem8  10651  tskuni  10796  monoord2  14101  seqz  14118  cshimadifsn0  14905  binom1dif  15926  bpolycl  16144  bpolysum  16145  bpolydiflem  16146  bitsres  16569  prdshom  17558  imasless  17632  cntzval  19454  f1omvdmvd  19576  f1omvdconj  19579  pmtrfb  19598  symggen  19603  symggen2  19604  psgnunilem1  19626  gsumzaddlem  20054  rngcbas  20789  ringcbas  20818  isdrngd  20937  isdrngdOLD  20939  lspextmo  21246  znleval  21773  freshmansdream  21793  ordtcld1  23428  ordtcld2  23429  cnpnei  23495  cnntri  23502  cncls2  23504  cncls  23505  cnntr  23506  cncnp  23511  cndis  23522  paste  23525  cmpfi  23639  conncompcld  23665  1stcfb  23676  1stccnp  23694  cldllycmp  23727  llycmpkgen2  23782  kgencn  23788  kgencn3  23790  dfac14lem  23849  txdis1cn  23867  hausdiag  23877  txkgen  23884  qtopval2  23928  basqtop  23943  qtopcld  23945  qtopeu  23948  qtoprest  23949  imastopn  23952  hmeontr  24001  hmeoimaf1o  24002  cmphaushmeo  24032  ordthmeolem  24033  elfm3  24182  rnelfmlem  24184  rnelfm  24185  alexsubALTlem4  24282  cldsubg  24343  tgpconncompeqg  24344  tgpconncomp  24345  qustgpopn  24352  qustgplem  24353  tsmsf1o  24377  ucncn  24516  imasf1oxms  24721  blcld  24737  metustfbas  24789  cfilucfil  24791  metuel2  24797  icchmeo  25175  relcmpcmet  25552  minveclem4a  25664  nulmbl2  25770  icombl  25798  ioombl  25799  uniiccdif  25812  volivth  25841  mbfres2  25879  itg1addlem5  25934  itgsplitioo  26072  dvcobr  26180  dvcnvlem  26210  lhop1lem  26247  lhop  26250  dvcnvrelem2  26252  uc1pval  26372  mon1pval  26374  vieta1lem2  26550  basellem5  27329  onnolt  28539  f1otrg  29335  axlowdimlem13  29419  axcontlem10  29438  uhgrspansubgr  29759  vtxdun  29949  pthhashvtx  30202  pthdlem1  30239  eucrct2eupth  30733  ssmd1  32800  mdslj2i  32809  atcvat4i  32886  imadifxp  33082  nfpconfp  33113  2ndresdju  33130  ofpreima  33146  ofpreima2  33147  fsuppcurry1  33203  fsuppcurry2  33204  indpreima  33319  indf1ofs  33320  ccatws1f1olast  33402  gsumpart  33511  symgcom  33531  symgcom2  33532  pmtrcnel  33537  cycpmfvlem  33560  cycpmfv3  33563  elrgspnsubrunlem2  33696  elrspunidl  33864  idlinsubrg  33867  esplymhp  34086  esplyfval1  34091  esplyfvaln  34092  fldextrspunlsp  34192  qtophaus  34354  reff  34357  locfinreflem  34358  zarcmplem  34399  hauseqcn  34416  oms0  34816  eulerpartlemv  34883  eulerpartlemb  34887  eulerpartlemr  34893  eulerpartlemgs2  34899  eulerpartlemn  34900  ballotlemro  35042  bnj1253  35534  bnj1280  35537  onvfowev  35721  acycgr0v  35735  prclisacycgr  35738  subfacp1lem3  35769  cvmscld  35860  cvmsss2  35861  cvmliftmolem1  35868  cvmliftlem7  35878  cvmlift2lem9  35898  cvmlift3lem7  35912  fnessref  36984  tailf  37002  poimirlem3  38380  mbfresfi  38423  cnambfre  38425  itg2addnclem2  38429  mettrifi  38515  ismtyres  38566  isdrngo2  38716  press  39255  diaintclN  41939  dibintclN  42048  dihintcl  42225  dochocss  42247  mapdunirnN  42531  pw2f1ocnv  43886  wessf1ornlem  46025  monoord2xrv  46319  itgcoscmulx  46805  ibliooicc  46807  stoweidlem11  46847  stoweidlem34  46870  fourierdlem48  46990  fourierdlem49  46991  fourierdlem74  47016  tmachlem-agreeprod  47773  uniimaprimaeqfv  48290  elsetpreimafvssdm  48294  fdivmptf  49479  refdivmptf  49480  iscnrm3llem2  49884  imaidfu  50044