Theorem sstrid 3947

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

Syntax hints:   → wi 4   ⊆ wss 3903

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 3920

This theorem is referenced by:  difsymssdifssd  4218  wereu2  5629  sofld  6153  resssxp  6236  frpomin  6306  fimass  6690  fvmptss  6962  isofr2  7300  frxp  8078  fnse  8085  frxp2  8096  frxp3  8103  frrlem4  8241  frrlem13  8250  fprlem1  8252  smores2  8296  naddunif  8631  dffi3  9346  marypha1lem  9348  ordtypelem7  9441  ordtypelem8  9442  oismo  9457  unxpwdom2  9505  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  13618  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  xptrrel  14915  limsupgle  15412  limsupgre  15416  rlimres  15493  lo1res  15494  lo1resb  15499  rlimresb  15500  o1resb  15501  o1of2  15548  o1rlimmul  15554  isercolllem2  15601  isercoll  15603  climsup  15605  fprodntriv  15877  bitsinvp1  16388  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadasslem  16409  sadeq  16411  bitsres  16412  smuval2  16421  smupval  16427  smueqlem  16429  smumul  16432  1arith  16867  isstruct2  17088  setscom  17119  ressress  17186  imasvscafn  17470  imasless  17473  mrcssv  17549  isacs1i  17592  mreacs  17593  acsfn  17594  isacs4lem  18479  isacs5lem  18480  mgmhmima  18652  mhmima  18762  cntzmhm  19282  f1omvdconj  19387  f1omvdco2  19389  symgsssg  19408  symggen  19411  efgval  19658  gsumzaddlem  19862  gsumconst  19875  dmdprdd  19942  dprdfeq0  19965  dprdres  19971  dprdss  19972  dprdz  19973  subgdmdprd  19977  dprddisj2  19982  dprd2dlem1  19984  dprd2da  19985  dprd2d2  19987  dmdprdsplit2lem  19988  gsumle  20086  lmhmlsp  21013  lsppratlem4  21117  islbs3  21122  lbsextlem3  21127  znleval  21521  evpmss  21553  frlmsslsp  21763  lindff1  21787  lindfrn  21788  f1lindf  21789  lindfmm  21794  lsslindf  21797  mplcoe5  22007  mplind  22037  basdif0  22909  tgcl  22925  ppttop  22963  epttop  22965  ntrin  23017  mretopd  23048  neiptoptop  23087  cnclsi  23228  cnconst2  23239  cnrest2  23242  cnpresti  23244  cnprest2  23246  fiuncmp  23360  connsub  23377  connima  23381  iunconnlem  23383  1stcfb  23401  2ndc1stc  23407  2ndcdisj  23412  kgentopon  23494  llycmpkgen2  23506  1stckgenlem  23509  kgencn3  23514  ptclsg  23571  ptcnplem  23577  txtube  23596  hausdiag  23601  txkgen  23608  xkoco1cn  23613  xkoco2cn  23614  xkococnlem  23615  qtoptop2  23655  basqtop  23667  imastopn  23676  hmeores  23727  hmphdis  23752  ptcmpfi  23769  fbssfi  23793  filin  23810  infil  23819  fgtr  23846  elfm  23903  hausflim  23937  flimclslem  23940  fclscmp  23986  cnextcn  24023  tmdgsum2  24052  tgpconncomp  24069  ustexsym  24172  ustund  24178  ustimasn  24184  utoptop  24190  utopbas  24191  restutopopn  24194  blin2  24385  metustexhalf  24512  icccmplem2  24780  icccmplem3  24781  reconnlem2  24784  tcphcph  25205  fmcfil  25240  resscdrg  25326  ivthlem2  25421  ivthlem3  25422  ivth2  25424  ovolfiniun  25470  ovoliunlem1  25471  ismbl2  25496  nulmbl2  25505  unmbl  25506  shftmbl  25507  voliunlem1  25519  voliunlem2  25520  ioombl1lem4  25530  uniioombllem4  25555  uniioombllem5  25556  dyadmbllem  25568  dyadmbl  25569  mbflimsup  25635  i1fima  25647  i1fima2  25648  i1fadd  25664  itg1addlem4  25668  itg2splitlem  25717  itg2split  25718  ellimc3  25848  limcflflem  25849  limcflf  25850  limcresi  25854  limciun  25863  dvreslem  25878  dvres2lem  25879  dvres  25880  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvlip  25966  dvlip2  25968  c1liplem1  25969  dvivthlem1  25981  dvne0  25984  lhop1lem  25986  lhop  25989  dvcnvrelem1  25990  dvcnvrelem2  25991  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgsubstlem  26023  mdegleb  26037  mdeglt  26038  mdegldg  26039  mdegxrcl  26040  mdegcl  26042  ig1peu  26148  reeff1olem  26424  logccv  26640  rlimcnp2  26944  lgamgulmlem2  27008  ppisval  27082  prmdvdsfi  27085  mumul  27159  sqff1o  27160  chtlepsi  27185  chpub  27199  dchrisum0lem2a  27496  pntlem3  27588  nosupno  27683  noetalem1  27721  cutlt  27940  negsproplem2  28037  onsbnd  28289  ex-res  30528  htthlem  31004  chlejb1i  31563  ssmd2  32399  fz2ssnn0  32875  gsumpart  33156  gsumhashmul  33160  elrgspnsubrunlem2  33341  extvfvcl  33712  mplvrpmrhm  33723  esplyind  33751  vietalem  33755  locfinreflem  34017  sibfof  34517  sitgclbn  34520  sitgaddlemb  34525  eulerpartlemgu  34554  ballotlemsima  34693  reprinrn  34795  bnj1311  35199  fnrelpredd  35266  erdsze2lem2  35417  iccllysconn  35463  cvmopnlem  35491  msrf  35755  neiin  36545  neibastop1  36572  neibastop2lem  36573  topmeet  36577  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem11  37876  poimirlem12  37877  poimirlem16  37881  poimirlem19  37884  poimirlem30  37895  cnambfre  37913  itg2gt0cn  37920  sstotbnd2  38019  sstotbnd3  38021  ssbnd  38033  ismtyima  38048  heibor1lem  38054  idresssidinxp  38559  pmodlem2  40217  pmodN  40220  diaintclN  41428  djaclN  41506  dibintclN  41537  dicval  41546  dihoml4c  41746  djhcl  41770  infdesc  42995  isnacs2  43057  isnacs3  43061  diophrw  43110  pellfundre  43232  pellfundge  43233  pellfundlb  43235  pellfundglb  43236  fnwe2lem2  43402  lmhmfgima  43435  hbt  43481  omabs2  43683  nadd2rabord  43736  nadd1rabord  43740  cnvtrcl0  43976  trclrelexplem  44061  relexp0a  44066  isotone2  44399  imo72b2lem1  44519  tcfr  45313  modelaxreplem1  45328  wfac8prim  45352  climinf  45960  islptre  45973  limccog  45974  limcleqr  45996  limsupvaluz2  46090  itgcoscmulx  46321  ismbl3  46338  ismbl4  46345  stoweidlem27  46379  dirkercncflem2  46456  fourierdlem38  46497  fourierdlem49  46507  fourierdlem51  46509  fourierdlem54  46512  fourierdlem63  46521  fourierdlem68  46526  fourierdlem69  46527  fourierdlem70  46528  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem80  46538  fourierdlem84  46542  fourierdlem85  46543  fourierdlem88  46546  fourierdlem100  46558  fourierdlem101  46559  fourierdlem104  46562  fourierdlem107  46565  fourierdlem111  46569  fourierdlem112  46570  caragenel2d  46884  hoidmv1lelem3  46945  hspmbllem3  46980  sssmf  47090  smfrec  47141  smfsuplem1  47163