Theorem sstrid 4006

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

Syntax hints:   → wi 4   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3979

This theorem is referenced by:  difsymssdifssd  4269  wereu2  5685  sofld  6208  resssxp  6291  frpomin  6362  fimass  6756  fvmptss  7027  isofr2  7363  frxp  8149  fnse  8156  frxp2  8167  frxp3  8174  frrlem4  8312  frrlem13  8321  fprlem1  8323  smores2  8392  naddunif  8729  dffi3  9468  marypha1lem  9470  ordtypelem7  9561  ordtypelem8  9562  oismo  9577  unxpwdom2  9625  cantnfres  9714  oemapvali  9721  frmin  9786  frrlem15  9794  frrlem16  9795  tskwe  9987  acndom2  10091  dfac2a  10167  dfac12lem2  10182  cfle  10291  cofsmo  10306  coftr  10310  isf34lem5  10415  isf34lem7  10416  isf34lem6  10417  enfin1ai  10421  fin1a2lem12  10448  ttukeylem7  10552  alephexp1  10616  fpwwe2lem12  10679  fpwwe2  10680  canth4  10684  canthwelem  10687  pwfseqlem1  10695  pwfseqlem4  10699  fzossnn0  13726  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  xptrrel  15015  limsupgle  15509  limsupgre  15513  rlimres  15590  lo1res  15591  lo1resb  15596  rlimresb  15597  o1resb  15598  o1of2  15645  o1rlimmul  15651  isercolllem2  15698  isercoll  15700  climsup  15702  fprodntriv  15974  bitsinvp1  16482  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadasslem  16503  sadeq  16505  bitsres  16506  smuval2  16515  smupval  16521  smueqlem  16523  smumul  16526  1arith  16960  isstruct2  17182  setscom  17213  ressress  17293  imasvscafn  17583  imasless  17586  mrcssv  17658  isacs1i  17701  mreacs  17702  acsfn  17703  isacs4lem  18601  isacs5lem  18602  mgmhmima  18740  mhmima  18850  cntzmhm  19371  f1omvdconj  19478  f1omvdco2  19480  symgsssg  19499  symggen  19502  efgval  19749  gsumzaddlem  19953  gsumconst  19966  dmdprdd  20033  dprdfeq0  20056  dprdres  20062  dprdss  20063  dprdz  20064  subgdmdprd  20068  dprddisj2  20073  dprd2dlem1  20075  dprd2da  20076  dprd2d2  20078  dmdprdsplit2lem  20079  lmhmlsp  21065  lsppratlem4  21169  islbs3  21174  lbsextlem3  21179  znleval  21590  evpmss  21621  frlmsslsp  21833  lindff1  21857  lindfrn  21858  f1lindf  21859  lindfmm  21864  lsslindf  21867  mplcoe5  22075  mplind  22111  basdif0  22975  tgcl  22991  ppttop  23029  epttop  23031  ntrin  23084  mretopd  23115  neiptoptop  23154  cnclsi  23295  cnconst2  23306  cnrest2  23309  cnpresti  23311  cnprest2  23313  fiuncmp  23427  connsub  23444  connima  23448  iunconnlem  23450  1stcfb  23468  2ndc1stc  23474  2ndcdisj  23479  kgentopon  23561  llycmpkgen2  23573  1stckgenlem  23576  kgencn3  23581  ptclsg  23638  ptcnplem  23644  txtube  23663  hausdiag  23668  txkgen  23675  xkoco1cn  23680  xkoco2cn  23681  xkococnlem  23682  qtoptop2  23722  basqtop  23734  imastopn  23743  hmeores  23794  hmphdis  23819  ptcmpfi  23836  fbssfi  23860  filin  23877  infil  23886  fgtr  23913  elfm  23970  hausflim  24004  flimclslem  24007  fclscmp  24053  cnextcn  24090  tmdgsum2  24119  tgpconncomp  24136  ustexsym  24239  ustund  24245  ustimasn  24252  utoptop  24258  utopbas  24259  restutopopn  24262  blin2  24454  metustexhalf  24584  icccmplem2  24858  icccmplem3  24859  reconnlem2  24862  tcphcph  25284  fmcfil  25319  resscdrg  25405  ivthlem2  25500  ivthlem3  25501  ivth2  25503  ovolfiniun  25549  ovoliunlem1  25550  ismbl2  25575  nulmbl2  25584  unmbl  25585  shftmbl  25586  voliunlem1  25598  voliunlem2  25599  ioombl1lem4  25609  uniioombllem4  25634  uniioombllem5  25635  dyadmbllem  25647  dyadmbl  25648  mbflimsup  25714  i1fima  25726  i1fima2  25727  i1fadd  25743  itg1addlem4  25747  itg1addlem4OLD  25748  itg2splitlem  25797  itg2split  25798  ellimc3  25928  limcflflem  25929  limcflf  25930  limcresi  25934  limciun  25943  dvreslem  25958  dvres2lem  25959  dvres  25960  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvlip  26046  dvlip2  26048  c1liplem1  26049  dvivthlem1  26061  dvne0  26064  lhop1lem  26066  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubstlem  26103  mdegleb  26117  mdeglt  26118  mdegldg  26119  mdegxrcl  26120  mdegcl  26122  ig1peu  26228  reeff1olem  26504  logccv  26719  rlimcnp2  27023  lgamgulmlem2  27087  ppisval  27161  prmdvdsfi  27164  mumul  27238  sqff1o  27239  chtlepsi  27264  chpub  27278  dchrisum0lem2a  27575  pntlem3  27667  nosupno  27762  noetalem1  27800  cutlt  27980  negsproplem2  28075  ex-res  30469  htthlem  30945  chlejb1i  31504  ssmd2  32340  fz2ssnn0  32793  gsumpart  33042  gsumhashmul  33046  gsumle  33083  locfinreflem  33800  sibfof  34321  sitgclbn  34324  sitgaddlemb  34329  eulerpartlemgu  34358  ballotlemsima  34496  reprinrn  34611  bnj1311  35016  fnrelpredd  35081  erdsze2lem2  35188  iccllysconn  35234  cvmopnlem  35262  msrf  35526  neiin  36314  neibastop1  36341  neibastop2lem  36342  topmeet  36346  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem19  37625  poimirlem30  37636  cnambfre  37654  itg2gt0cn  37661  sstotbnd2  37760  sstotbnd3  37762  ssbnd  37774  ismtyima  37789  heibor1lem  37795  idresssidinxp  38289  pmodlem2  39829  pmodN  39832  diaintclN  41040  djaclN  41118  dibintclN  41149  dicval  41158  dihoml4c  41358  djhcl  41382  infdesc  42629  isnacs2  42693  isnacs3  42697  diophrw  42746  pellfundre  42868  pellfundge  42869  pellfundlb  42871  pellfundglb  42872  fnwe2lem2  43039  lmhmfgima  43072  hbt  43118  omabs2  43321  nadd2rabord  43374  nadd1rabord  43378  cnvtrcl0  43615  trclrelexplem  43700  relexp0a  43705  isotone2  44038  imo72b2lem1  44158  modelaxreplem1  44942  climinf  45561  islptre  45574  limccog  45575  limcleqr  45599  limsupvaluz2  45693  itgcoscmulx  45924  ismbl3  45941  ismbl4  45948  stoweidlem27  45982  dirkercncflem2  46059  fourierdlem38  46100  fourierdlem49  46110  fourierdlem51  46112  fourierdlem54  46115  fourierdlem63  46124  fourierdlem68  46129  fourierdlem69  46130  fourierdlem70  46131  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem80  46141  fourierdlem84  46145  fourierdlem85  46146  fourierdlem88  46149  fourierdlem100  46161  fourierdlem101  46162  fourierdlem104  46165  fourierdlem107  46168  fourierdlem111  46172  fourierdlem112  46173  caragenel2d  46487  hoidmv1lelem3  46548  hspmbllem3  46583  sssmf  46693  smfrec  46744  smfsuplem1  46766