Theorem sstrid 3924

Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)

Hypotheses

Ref	Expression
sstrid.1	⊢ 𝐴 ⊆ 𝐵
sstrid.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
sstrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrid

Step	Hyp	Ref	Expression
1		sstrid.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3		sstrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	sstrd 3923	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3901

This theorem is used by:  difsymssdifssd  4212  wereu2  5653  sofld  6192  resssxp  6291  frpomin  6364  fimass  6755  fvmptss  7032  isofr2  7378  ovmptss  8132  frxp  8168  fnse  8180  frxp2  8191  frxp3  8198  frrlem4  8338  frrlem13  8347  fprlem1  8349  smores2  8393  naddunif  8734  dffi3  9453  marypha1lem  9455  ordtypelem7  9548  ordtypelem8  9549  oismo  9564  unxpwdom2  9612  cantnfres  9708  oemapvali  9715  frmin  9783  frrlem15  9791  frrlem16  9792  tskwe  10061  acndom2  10163  dfac2a  10238  dfac12lem2  10253  cfle  10361  cofsmo  10377  coftr  10381  isf34lem5  10486  isf34lem7  10487  isf34lem6  10488  enfin1ai  10492  fin1a2lem12  10519  ttukeylem7  10623  alephexp1  10694  fpwwe2lem12  10757  fpwwe2  10758  canth4  10762  canthwelem  10765  pwfseqlem1  10773  pwfseqlem4  10777  fzossnn0  13855  fsuppmapnn0fiublem  14163  fsuppmapnn0fiub  14164  xptrrel  15165  limsupgle  15676  limsupgre  15680  rlimres  15757  lo1res  15758  lo1resb  15763  rlimresb  15764  o1resb  15765  o1of2  15812  o1rlimmul  15818  isercolllem2  15865  isercoll  15867  climsup  15869  fprodntriv  16141  bitsinvp1  16651  sadcaddlem  16659  sadadd2lem  16661  sadadd3  16663  sadasslem  16672  sadeq  16674  bitsres  16675  smuval2  16684  smupval  16690  smueqlem  16692  smumul  16695  1arith  17137  isstruct2  17359  setscom  17390  ressress  17457  imasvscafn  17741  imasless  17744  mrcssv  17820  isacs1i  17863  mreacs  17864  acsfn  17865  isacs4lem  18750  isacs5lem  18751  mgmhmima  18936  mhmima  19053  cntzmhm  19588  f1omvdconj  19693  f1omvdco2  19695  symgsssg  19714  symggen  19717  efgval  19964  gsumzaddlem  20168  gsumconst  20181  dmdprdd  20248  dprdfeq0  20271  dprdres  20277  dprdss  20278  dprdz  20279  subgdmdprd  20283  dprddisj2  20288  dprd2dlem1  20290  dprd2da  20291  dprd2d2  20293  dmdprdsplit2lem  20294  gsumle  20392  lmhmlsp  21357  lsppratlem4  21461  islbs3  21466  lbsextlem3  21471  znleval  21893  evpmss  21925  frlmsslsp  22135  lindff1  22159  lindfrn  22160  f1lindf  22161  lindfmm  22166  lsslindf  22169  mplcoe5  22382  mplind  22412  basdif0  23304  tgcl  23320  ppttop  23358  epttop  23360  ntrin  23412  mretopd  23443  neiptoptop  23482  cnclsi  23623  cnconst2  23634  cnrest2  23637  cnpresti  23639  cnprest2  23641  fiuncmp  23755  connsub  23772  connima  23776  iunconnlem  23778  1stcfb  23796  2ndc1stc  23802  2ndcdisj  23808  kgentopon  23890  llycmpkgen2  23902  1stckgenlem  23905  kgencn3  23910  ptclsg  23967  ptcnplem  23973  txtube  23992  hausdiag  23997  txkgen  24004  xkoco1cn  24009  xkoco2cn  24010  xkococnlem  24011  qtoptop2  24051  basqtop  24063  imastopn  24072  hmeores  24123  hmphdis  24148  ptcmpfi  24165  fbssfi  24189  filin  24206  infil  24215  fgtr  24242  elfm  24299  hausflim  24333  flimclslem  24336  fclscmp  24382  cnextcn  24419  tmdgsum2  24448  tgpconncomp  24465  ustexsym  24568  ustund  24574  ustimasn  24580  utoptop  24586  utopbas  24587  restutopopn  24590  blin2  24781  metustexhalf  24908  icccmplem2  25176  icccmplem3  25177  reconnlem2  25180  tcphcph  25591  fmcfil  25626  resscdrg  25712  ivthlem2  25806  ivthlem3  25807  ivth2  25809  ovolfiniun  25855  ovoliunlem1  25856  ismbl2  25881  nulmbl2  25890  unmbl  25891  shftmbl  25892  voliunlem1  25904  voliunlem2  25905  ioombl1lem4  25915  uniioombllem4  25940  uniioombllem5  25941  dyadmbllem  25953  dyadmbl  25954  mbflimsup  26020  i1fima  26032  i1fima2  26033  i1fadd  26049  itg1addlem4  26053  itg2splitlem  26102  itg2split  26103  ellimc3  26232  limcflflem  26233  limcflf  26234  limcresi  26238  limciun  26247  dvreslem  26262  dvres2lem  26263  dvres  26264  dvaddbr  26291  dvmulbr  26292  dvlip  26346  dvlip2  26348  c1liplem1  26349  dvivthlem1  26361  dvne0  26364  lhop1lem  26366  lhop  26369  dvcnvrelem1  26370  dvcnvrelem2  26371  dvfsumle  26374  dvfsumabs  26376  dvfsumlem2  26380  itgsubstlem  26401  mdegleb  26415  mdeglt  26416  mdegldg  26417  mdegxrcl  26418  mdegcl  26420  ig1peu  26526  reeff1olem  26806  logccv  27024  rlimcnp2  27327  lgamgulmlem2  27390  ppisval  27464  prmdvdsfi  27467  mumul  27541  sqff1o  27542  chtlepsi  27566  chpub  27580  dchrisum0lem2a  27877  pntlem3  27969  infdesc  28000  nosupno  28093  noetalem1  28131  cutlt  28351  negsproplem2  28448  onsbnd  28700  cgrabasimass  29411  ex-res  31075  htthlem  31552  chlejb1i  32111  ssmd2  32947  fz2ssnn0  33450  gsumpart  33700  gsumhashmul  33704  elrgspnsubrunlem2  33885  extvfvcl  34251  mplvrpmrhm  34262  esplyind  34290  vietalem  34294  locfinreflem  34555  sibfof  35055  sitgclbn  35058  sitgaddlemb  35063  eulerpartlemgu  35092  ballotlemsima  35231  reprinrn  35330  bnj1311  35737  fnrelpredd  35817  j0le  36032  k1le  36034  k2le  36035  erdsze2lem2  36149  iccllysconn  36195  cvmopnlem  36223  msrf  36487  neiin  37311  neibastop1  37338  neibastop2lem  37339  topmeet  37343  ttciunun  37490  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem11  38754  poimirlem12  38755  poimirlem16  38759  poimirlem19  38762  poimirlem30  38773  cnambfre  38791  itg2gt0cn  38798  sstotbnd2  38911  sstotbnd3  38913  ssbnd  38925  ismtyima  38940  heibor1lem  38946  idresssidinxp  39449  pmodlem2  41107  pmodN  41110  diaintclN  42318  djaclN  42396  dibintclN  42427  dicval  42436  dihoml4c  42636  djhcl  42660  isnacs2  43921  isnacs3  43925  diophrw  43974  pellfundre  44092  pellfundge  44093  pellfundlb  44095  pellfundglb  44096  lmhmfgima  44290  hbt  44335  omabs2  44537  nadd2rabord  44590  nadd1rabord  44594  cnvtrcl0  44829  trclrelexplem  44914  relexp0a  44919  isotone2  45252  imo72b2lem1  45372  tcfr  46159  modelaxreplem1  46174  wfac8prim  46198  climinf  46833  islptre  46846  limccog  46847  limcleqr  46869  limsupvaluz2  46963  itgcoscmulx  47194  ismbl3  47211  ismbl4  47218  stoweidlem27  47252  dirkercncflem2  47329  fourierdlem38  47370  fourierdlem51  47382  fourierdlem54  47385  fourierdlem63  47394  fourierdlem68  47399  fourierdlem69  47400  fourierdlem70  47401  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem80  47411  fourierdlem84  47415  fourierdlem85  47416  fourierdlem88  47419  fourierdlem100  47431  fourierdlem101  47432  fourierdlem104  47435  fourierdlem107  47438  fourierdlem111  47442  fourierdlem112  47443  caragenel2d  47757  hoidmv1lelem3  47818  hspmbllem3  47853  sssmf  47963  smfrec  48014  smfsuplem1  48036