Theorem sstrid 3933

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

Syntax hints:   → wi 4   ⊆ wss 3889

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

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

This theorem is referenced by:  difsymssdifssd  4204  wereu2  5628  sofld  6151  resssxp  6234  frpomin  6304  fimass  6688  fvmptss  6960  isofr2  7299  frxp  8076  fnse  8083  frxp2  8094  frxp3  8101  frrlem4  8239  frrlem13  8248  fprlem1  8250  smores2  8294  naddunif  8629  dffi3  9344  marypha1lem  9346  ordtypelem7  9439  ordtypelem8  9440  oismo  9455  unxpwdom2  9503  cantnfres  9598  oemapvali  9605  frmin  9673  frrlem15  9681  frrlem16  9682  tskwe  9874  acndom2  9976  dfac2a  10052  dfac12lem2  10067  cfle  10176  cofsmo  10191  coftr  10195  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  enfin1ai  10306  fin1a2lem12  10333  ttukeylem7  10437  alephexp1  10502  fpwwe2lem12  10565  fpwwe2  10566  canth4  10570  canthwelem  10573  pwfseqlem1  10581  pwfseqlem4  10585  fzossnn0  13645  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  xptrrel  14942  limsupgle  15439  limsupgre  15443  rlimres  15520  lo1res  15521  lo1resb  15526  rlimresb  15527  o1resb  15528  o1of2  15575  o1rlimmul  15581  isercolllem2  15628  isercoll  15630  climsup  15632  fprodntriv  15907  bitsinvp1  16418  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadasslem  16439  sadeq  16441  bitsres  16442  smuval2  16451  smupval  16457  smueqlem  16459  smumul  16462  1arith  16898  isstruct2  17119  setscom  17150  ressress  17217  imasvscafn  17501  imasless  17504  mrcssv  17580  isacs1i  17623  mreacs  17624  acsfn  17625  isacs4lem  18510  isacs5lem  18511  mgmhmima  18683  mhmima  18793  cntzmhm  19316  f1omvdconj  19421  f1omvdco2  19423  symgsssg  19442  symggen  19445  efgval  19692  gsumzaddlem  19896  gsumconst  19909  dmdprdd  19976  dprdfeq0  19999  dprdres  20005  dprdss  20006  dprdz  20007  subgdmdprd  20011  dprddisj2  20016  dprd2dlem1  20018  dprd2da  20019  dprd2d2  20021  dmdprdsplit2lem  20022  gsumle  20120  lmhmlsp  21044  lsppratlem4  21148  islbs3  21153  lbsextlem3  21158  znleval  21534  evpmss  21566  frlmsslsp  21776  lindff1  21800  lindfrn  21801  f1lindf  21802  lindfmm  21807  lsslindf  21810  mplcoe5  22018  mplind  22048  basdif0  22918  tgcl  22934  ppttop  22972  epttop  22974  ntrin  23026  mretopd  23057  neiptoptop  23096  cnclsi  23237  cnconst2  23248  cnrest2  23251  cnpresti  23253  cnprest2  23255  fiuncmp  23369  connsub  23386  connima  23390  iunconnlem  23392  1stcfb  23410  2ndc1stc  23416  2ndcdisj  23421  kgentopon  23503  llycmpkgen2  23515  1stckgenlem  23518  kgencn3  23523  ptclsg  23580  ptcnplem  23586  txtube  23605  hausdiag  23610  txkgen  23617  xkoco1cn  23622  xkoco2cn  23623  xkococnlem  23624  qtoptop2  23664  basqtop  23676  imastopn  23685  hmeores  23736  hmphdis  23761  ptcmpfi  23778  fbssfi  23802  filin  23819  infil  23828  fgtr  23855  elfm  23912  hausflim  23946  flimclslem  23949  fclscmp  23995  cnextcn  24032  tmdgsum2  24061  tgpconncomp  24078  ustexsym  24181  ustund  24187  ustimasn  24193  utoptop  24199  utopbas  24200  restutopopn  24203  blin2  24394  metustexhalf  24521  icccmplem2  24789  icccmplem3  24790  reconnlem2  24793  tcphcph  25204  fmcfil  25239  resscdrg  25325  ivthlem2  25419  ivthlem3  25420  ivth2  25422  ovolfiniun  25468  ovoliunlem1  25469  ismbl2  25494  nulmbl2  25503  unmbl  25504  shftmbl  25505  voliunlem1  25517  voliunlem2  25518  ioombl1lem4  25528  uniioombllem4  25553  uniioombllem5  25554  dyadmbllem  25566  dyadmbl  25567  mbflimsup  25633  i1fima  25645  i1fima2  25646  i1fadd  25662  itg1addlem4  25666  itg2splitlem  25715  itg2split  25716  ellimc3  25846  limcflflem  25847  limcflf  25848  limcresi  25852  limciun  25861  dvreslem  25876  dvres2lem  25877  dvres  25878  dvaddbr  25905  dvmulbr  25906  dvlip  25960  dvlip2  25962  c1liplem1  25963  dvivthlem1  25975  dvne0  25978  lhop1lem  25980  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvfsumle  25988  dvfsumabs  25990  dvfsumlem2  25994  itgsubstlem  26015  mdegleb  26029  mdeglt  26030  mdegldg  26031  mdegxrcl  26032  mdegcl  26034  ig1peu  26140  reeff1olem  26411  logccv  26627  rlimcnp2  26930  lgamgulmlem2  26993  ppisval  27067  prmdvdsfi  27070  mumul  27144  sqff1o  27145  chtlepsi  27169  chpub  27183  dchrisum0lem2a  27480  pntlem3  27572  nosupno  27667  noetalem1  27705  cutlt  27924  negsproplem2  28021  onsbnd  28273  ex-res  30511  htthlem  30988  chlejb1i  31547  ssmd2  32383  fz2ssnn0  32858  gsumpart  33124  gsumhashmul  33128  elrgspnsubrunlem2  33309  extvfvcl  33680  mplvrpmrhm  33691  esplyind  33719  vietalem  33723  locfinreflem  33984  sibfof  34484  sitgclbn  34487  sitgaddlemb  34492  eulerpartlemgu  34521  ballotlemsima  34660  reprinrn  34762  bnj1311  35166  fnrelpredd  35234  erdsze2lem2  35386  iccllysconn  35432  cvmopnlem  35460  msrf  35724  neiin  36514  neibastop1  36541  neibastop2lem  36542  topmeet  36546  ttciunun  36693  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem19  37960  poimirlem30  37971  cnambfre  37989  itg2gt0cn  37996  sstotbnd2  38095  sstotbnd3  38097  ssbnd  38109  ismtyima  38124  heibor1lem  38130  idresssidinxp  38635  pmodlem2  40293  pmodN  40296  diaintclN  41504  djaclN  41582  dibintclN  41613  dicval  41622  dihoml4c  41822  djhcl  41846  infdesc  43076  isnacs2  43138  isnacs3  43142  diophrw  43191  pellfundre  43309  pellfundge  43310  pellfundlb  43312  pellfundglb  43313  fnwe2lem2  43479  lmhmfgima  43512  hbt  43558  omabs2  43760  nadd2rabord  43813  nadd1rabord  43817  cnvtrcl0  44053  trclrelexplem  44138  relexp0a  44143  isotone2  44476  imo72b2lem1  44596  tcfr  45390  modelaxreplem1  45405  wfac8prim  45429  climinf  46036  islptre  46049  limccog  46050  limcleqr  46072  limsupvaluz2  46166  itgcoscmulx  46397  ismbl3  46414  ismbl4  46421  stoweidlem27  46455  dirkercncflem2  46532  fourierdlem38  46573  fourierdlem49  46583  fourierdlem51  46585  fourierdlem54  46588  fourierdlem63  46597  fourierdlem68  46602  fourierdlem69  46603  fourierdlem70  46604  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem80  46614  fourierdlem84  46618  fourierdlem85  46619  fourierdlem88  46622  fourierdlem100  46634  fourierdlem101  46635  fourierdlem104  46638  fourierdlem107  46641  fourierdlem111  46645  fourierdlem112  46646  caragenel2d  46960  hoidmv1lelem3  47021  hspmbllem3  47056  sssmf  47166  smfrec  47217  smfsuplem1  47239