Theorem sstrid 3993

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

Syntax hints:   → wi 4   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  difsymssdifssd  4253  wereu2  5673  sofld  6184  resssxp  6267  frpomin  6339  fimass  6736  fvmptss  7008  fimacnvOLD  7070  isofr2  7338  frxp  8109  fnse  8116  frxp2  8127  frxp3  8134  frrlem4  8271  frrlem13  8280  fprlem1  8282  smores2  8351  naddunif  8689  dffi3  9423  marypha1lem  9425  ordtypelem7  9516  ordtypelem8  9517  oismo  9532  unxpwdom2  9580  cantnfres  9669  oemapvali  9676  frmin  9741  frrlem15  9749  frrlem16  9750  tskwe  9942  acndom2  10046  dfac2a  10121  dfac12lem2  10136  cfle  10246  cofsmo  10261  coftr  10265  isf34lem5  10370  isf34lem7  10371  isf34lem6  10372  enfin1ai  10376  fin1a2lem12  10403  ttukeylem7  10507  alephexp1  10571  fpwwe2lem12  10634  fpwwe2  10635  canth4  10639  canthwelem  10642  pwfseqlem1  10650  pwfseqlem4  10654  fzossnn0  13660  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  xptrrel  14924  limsupgle  15418  limsupgre  15422  rlimres  15499  lo1res  15500  lo1resb  15505  rlimresb  15506  o1resb  15507  o1of2  15554  o1rlimmul  15560  isercolllem2  15609  isercoll  15611  climsup  15613  fprodntriv  15883  bitsinvp1  16387  sadcaddlem  16395  sadadd2lem  16397  sadadd3  16399  sadasslem  16408  sadeq  16410  bitsres  16411  smuval2  16420  smupval  16426  smueqlem  16428  smumul  16431  1arith  16857  isstruct2  17079  setscom  17110  ressress  17190  imasvscafn  17480  imasless  17483  mrcssv  17555  isacs1i  17598  mreacs  17599  acsfn  17600  isacs4lem  18494  isacs5lem  18495  mhmima  18703  cntzmhm  19200  f1omvdconj  19309  f1omvdco2  19311  symgsssg  19330  symggen  19333  efgval  19580  gsumzaddlem  19784  gsumconst  19797  dmdprdd  19864  dprdfeq0  19887  dprdres  19893  dprdss  19894  dprdz  19895  subgdmdprd  19899  dprddisj2  19904  dprd2dlem1  19906  dprd2da  19907  dprd2d2  19909  dmdprdsplit2lem  19910  lmhmlsp  20653  lsppratlem4  20756  islbs3  20761  lbsextlem3  20766  znleval  21102  evpmss  21131  frlmsslsp  21343  lindff1  21367  lindfrn  21368  f1lindf  21369  lindfmm  21374  lsslindf  21377  mplcoe5  21587  mplind  21623  basdif0  22448  tgcl  22464  ppttop  22502  epttop  22504  ntrin  22557  mretopd  22588  neiptoptop  22627  cnclsi  22768  cnconst2  22779  cnrest2  22782  cnpresti  22784  cnprest2  22786  fiuncmp  22900  connsub  22917  connima  22921  iunconnlem  22923  1stcfb  22941  2ndc1stc  22947  2ndcdisj  22952  kgentopon  23034  llycmpkgen2  23046  1stckgenlem  23049  kgencn3  23054  ptclsg  23111  ptcnplem  23117  txtube  23136  hausdiag  23141  txkgen  23148  xkoco1cn  23153  xkoco2cn  23154  xkococnlem  23155  qtoptop2  23195  basqtop  23207  imastopn  23216  hmeores  23267  hmphdis  23292  ptcmpfi  23309  fbssfi  23333  filin  23350  infil  23359  fgtr  23386  elfm  23443  hausflim  23477  flimclslem  23480  fclscmp  23526  cnextcn  23563  tmdgsum2  23592  tgpconncomp  23609  ustexsym  23712  ustund  23718  ustimasn  23725  utoptop  23731  utopbas  23732  restutopopn  23735  blin2  23927  metustexhalf  24057  icccmplem2  24331  icccmplem3  24332  reconnlem2  24335  tcphcph  24746  fmcfil  24781  resscdrg  24867  ivthlem2  24961  ivthlem3  24962  ivth2  24964  ovolfiniun  25010  ovoliunlem1  25011  ismbl2  25036  nulmbl2  25045  unmbl  25046  shftmbl  25047  voliunlem1  25059  voliunlem2  25060  ioombl1lem4  25070  uniioombllem4  25095  uniioombllem5  25096  dyadmbllem  25108  dyadmbl  25109  mbflimsup  25175  i1fima  25187  i1fima2  25188  i1fadd  25204  itg1addlem4  25208  itg1addlem4OLD  25209  itg2splitlem  25258  itg2split  25259  ellimc3  25388  limcflflem  25389  limcflf  25390  limcresi  25394  limciun  25403  dvreslem  25418  dvres2lem  25419  dvres  25420  dvaddbr  25447  dvmulbr  25448  dvlip  25502  dvlip2  25504  c1liplem1  25505  dvivthlem1  25517  dvne0  25520  lhop1lem  25522  lhop  25525  dvcnvrelem1  25526  dvcnvrelem2  25527  dvfsumle  25530  dvfsumabs  25532  dvfsumlem2  25536  itgsubstlem  25557  mdegleb  25574  mdeglt  25575  mdegldg  25576  mdegxrcl  25577  mdegcl  25579  ig1peu  25681  reeff1olem  25950  logccv  26163  rlimcnp2  26461  lgamgulmlem2  26524  ppisval  26598  prmdvdsfi  26601  mumul  26675  sqff1o  26676  chtlepsi  26699  chpub  26713  dchrisum0lem2a  27010  pntlem3  27102  nosupno  27196  noetalem1  27234  cutlt  27409  negsproplem2  27493  ex-res  29684  htthlem  30158  chlejb1i  30717  ssmd2  31553  fz2ssnn0  31984  gsumpart  32195  gsumhashmul  32196  gsumle  32230  locfinreflem  32809  sibfof  33328  sitgclbn  33331  sitgaddlemb  33336  eulerpartlemgu  33365  ballotlemsima  33503  reprinrn  33619  bnj1311  34024  fnrelpredd  34081  erdsze2lem2  34184  iccllysconn  34230  cvmopnlem  34258  msrf  34522  gg-dvmulbr  35164  gg-dvfsumle  35171  gg-dvfsumlem2  35172  neiin  35206  neibastop1  35233  neibastop2lem  35234  topmeet  35238  poimirlem1  36478  poimirlem2  36479  poimirlem3  36480  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem19  36496  poimirlem30  36507  cnambfre  36525  itg2gt0cn  36532  sstotbnd2  36631  sstotbnd3  36633  ssbnd  36645  ismtyima  36660  heibor1lem  36666  idresssidinxp  37166  pmodlem2  38707  pmodN  38710  diaintclN  39918  djaclN  39996  dibintclN  40027  dicval  40036  dihoml4c  40236  djhcl  40260  infdesc  41382  isnacs2  41430  isnacs3  41434  diophrw  41483  pellfundre  41605  pellfundge  41606  pellfundlb  41608  pellfundglb  41609  fnwe2lem2  41779  lmhmfgima  41812  hbt  41858  omabs2  42068  nadd2rabord  42121  nadd1rabord  42125  cnvtrcl0  42363  trclrelexplem  42448  relexp0a  42453  isotone2  42786  imo72b2lem1  42907  climinf  44309  islptre  44322  limccog  44323  limcleqr  44347  itgcoscmulx  44672  ismbl3  44689  ismbl4  44696  stoweidlem27  44730  dirkercncflem2  44807  fourierdlem38  44848  fourierdlem49  44858  fourierdlem51  44860  fourierdlem54  44863  fourierdlem63  44872  fourierdlem68  44877  fourierdlem69  44878  fourierdlem70  44879  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem80  44889  fourierdlem84  44893  fourierdlem85  44894  fourierdlem88  44897  fourierdlem100  44909  fourierdlem101  44910  fourierdlem104  44913  fourierdlem107  44916  fourierdlem111  44920  fourierdlem112  44921  caragenel2d  45235  hoidmv1lelem3  45296  hspmbllem3  45331  sssmf  45441  smfrec  45492  smfsuplem1  45514  mgmhmima  46559