Theorem sstrid 3950

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

Syntax hints:   → wi 4   ⊆ wss 3907

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3924

This theorem is referenced by:  difsymssdifssd  4219  wereu2  5648  sofld  6176  resssxp  6260  frpomin  6330  fimass  6716  fvmptss  6992  isofr2  7332  frxp  8110  fnse  8117  frxp2  8128  frxp3  8135  frrlem4  8274  frrlem13  8283  fprlem1  8285  smores2  8329  naddunif  8668  dffi3  9379  marypha1lem  9381  ordtypelem7  9474  ordtypelem8  9475  oismo  9490  unxpwdom2  9538  cantnfres  9634  oemapvali  9641  frmin  9709  frrlem15  9717  frrlem16  9718  tskwe  9924  acndom2  10026  dfac2a  10101  dfac12lem2  10116  cfle  10225  cofsmo  10241  coftr  10245  isf34lem5  10350  isf34lem7  10351  isf34lem6  10352  enfin1ai  10356  fin1a2lem12  10383  ttukeylem7  10487  alephexp1  10552  fpwwe2lem12  10615  fpwwe2  10616  canth4  10620  canthwelem  10623  pwfseqlem1  10631  pwfseqlem4  10635  fzossnn0  13707  fsuppmapnn0fiublem  14014  fsuppmapnn0fiub  14015  xptrrel  15005  limsupgle  15516  limsupgre  15520  rlimres  15597  lo1res  15598  lo1resb  15603  rlimresb  15604  o1resb  15605  o1of2  15652  o1rlimmul  15658  isercolllem2  15705  isercoll  15707  climsup  15709  fprodntriv  15984  bitsinvp1  16495  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadasslem  16516  sadeq  16518  bitsres  16519  smuval2  16528  smupval  16534  smueqlem  16536  smumul  16539  1arith  16975  isstruct2  17197  setscom  17228  ressress  17295  imasvscafn  17579  imasless  17582  mrcssv  17658  isacs1i  17701  mreacs  17702  acsfn  17703  isacs4lem  18588  isacs5lem  18589  mgmhmima  18761  mhmima  18872  cntzmhm  19399  f1omvdconj  19504  f1omvdco2  19506  symgsssg  19525  symggen  19528  efgval  19775  gsumzaddlem  19979  gsumconst  19992  dmdprdd  20059  dprdfeq0  20082  dprdres  20088  dprdss  20089  dprdz  20090  subgdmdprd  20094  dprddisj2  20099  dprd2dlem1  20101  dprd2da  20102  dprd2d2  20104  dmdprdsplit2lem  20105  gsumle  20203  lmhmlsp  21136  lsppratlem4  21240  islbs3  21245  lbsextlem3  21250  znleval  21661  evpmss  21693  frlmsslsp  21903  lindff1  21927  lindfrn  21928  f1lindf  21929  lindfmm  21934  lsslindf  21937  mplcoe5  22148  mplind  22178  basdif0  23067  tgcl  23083  ppttop  23121  epttop  23123  ntrin  23175  mretopd  23206  neiptoptop  23245  cnclsi  23386  cnconst2  23397  cnrest2  23400  cnpresti  23402  cnprest2  23404  fiuncmp  23518  connsub  23535  connima  23539  iunconnlem  23541  1stcfb  23559  2ndc1stc  23565  2ndcdisj  23570  kgentopon  23652  llycmpkgen2  23664  1stckgenlem  23667  kgencn3  23672  ptclsg  23729  ptcnplem  23735  txtube  23754  hausdiag  23759  txkgen  23766  xkoco1cn  23771  xkoco2cn  23772  xkococnlem  23773  qtoptop2  23813  basqtop  23825  imastopn  23834  hmeores  23885  hmphdis  23910  ptcmpfi  23927  fbssfi  23951  filin  23968  infil  23977  fgtr  24004  elfm  24061  hausflim  24095  flimclslem  24098  fclscmp  24144  cnextcn  24181  tmdgsum2  24210  tgpconncomp  24227  ustexsym  24330  ustund  24336  ustimasn  24342  utoptop  24348  utopbas  24349  restutopopn  24352  blin2  24543  metustexhalf  24670  icccmplem2  24938  icccmplem3  24939  reconnlem2  24942  tcphcph  25353  fmcfil  25388  resscdrg  25474  ivthlem2  25568  ivthlem3  25569  ivth2  25571  ovolfiniun  25617  ovoliunlem1  25618  ismbl2  25643  nulmbl2  25652  unmbl  25653  shftmbl  25654  voliunlem1  25666  voliunlem2  25667  ioombl1lem4  25677  uniioombllem4  25702  uniioombllem5  25703  dyadmbllem  25715  dyadmbl  25716  mbflimsup  25782  i1fima  25794  i1fima2  25795  i1fadd  25811  itg1addlem4  25815  itg2splitlem  25864  itg2split  25865  ellimc3  25995  limcflflem  25996  limcflf  25997  limcresi  26001  limciun  26010  dvreslem  26025  dvres2lem  26026  dvres  26027  dvaddbr  26054  dvmulbr  26055  dvlip  26109  dvlip2  26111  c1liplem1  26112  dvivthlem1  26124  dvne0  26127  lhop1lem  26129  lhop  26132  dvcnvrelem1  26133  dvcnvrelem2  26134  dvfsumle  26137  dvfsumabs  26139  dvfsumlem2  26143  itgsubstlem  26164  mdegleb  26178  mdeglt  26179  mdegldg  26180  mdegxrcl  26181  mdegcl  26183  ig1peu  26289  reeff1olem  26563  logccv  26782  rlimcnp2  27085  lgamgulmlem2  27148  ppisval  27222  prmdvdsfi  27225  mumul  27299  sqff1o  27300  chtlepsi  27324  chpub  27338  dchrisum0lem2a  27635  pntlem3  27727  nosupno  27821  noetalem1  27859  cutlt  28079  negsproplem2  28176  onsbnd  28428  ex-res  30697  htthlem  31174  chlejb1i  31733  ssmd2  32569  fz2ssnn0  33038  gsumpart  33291  gsumhashmul  33295  elrgspnsubrunlem2  33476  extvfvcl  33838  mplvrpmrhm  33849  esplyind  33877  vietalem  33881  locfinreflem  34142  sibfof  34642  sitgclbn  34645  sitgaddlemb  34650  eulerpartlemgu  34679  ballotlemsima  34818  reprinrn  34917  bnj1311  35324  fnrelpredd  35392  erdsze2lem2  35562  iccllysconn  35608  cvmopnlem  35636  msrf  35900  neiin  36700  neibastop1  36727  neibastop2lem  36728  topmeet  36732  ttciunun  36879  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem11  38137  poimirlem12  38138  poimirlem16  38142  poimirlem19  38145  poimirlem30  38156  cnambfre  38174  itg2gt0cn  38181  sstotbnd2  38280  sstotbnd3  38282  ssbnd  38294  ismtyima  38309  heibor1lem  38315  idresssidinxp  38820  pmodlem2  40478  pmodN  40481  diaintclN  41689  djaclN  41767  dibintclN  41798  dicval  41807  dihoml4c  42007  djhcl  42031  infdesc  43232  isnacs2  43294  isnacs3  43298  diophrw  43347  pellfundre  43465  pellfundge  43466  pellfundlb  43468  pellfundglb  43469  fnwe2lem2  43635  lmhmfgima  43668  hbt  43714  omabs2  43916  nadd2rabord  43969  nadd1rabord  43973  cnvtrcl0  44209  trclrelexplem  44294  relexp0a  44299  isotone2  44632  imo72b2lem1  44752  tcfr  45531  modelaxreplem1  45546  wfac8prim  45570  climinf  46181  islptre  46194  limccog  46195  limcleqr  46217  limsupvaluz2  46311  itgcoscmulx  46542  ismbl3  46559  ismbl4  46566  stoweidlem27  46600  dirkercncflem2  46677  fourierdlem38  46718  fourierdlem51  46730  fourierdlem54  46733  fourierdlem63  46742  fourierdlem68  46747  fourierdlem69  46748  fourierdlem70  46749  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem80  46759  fourierdlem84  46763  fourierdlem85  46764  fourierdlem88  46767  fourierdlem100  46779  fourierdlem101  46780  fourierdlem104  46783  fourierdlem107  46786  fourierdlem111  46790  fourierdlem112  46791  caragenel2d  47105  hoidmv1lelem3  47166  hspmbllem3  47201  sssmf  47311  smfrec  47362  smfsuplem1  47384