Theorem sstrid 3945

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

Syntax hints:   → wi 4   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3919

This theorem is referenced by:  difsymssdifssd  4214  wereu2  5640  sofld  6167  resssxp  6251  frpomin  6321  fimass  6706  fvmptss  6982  isofr2  7322  frxp  8099  fnse  8106  frxp2  8117  frxp3  8124  frrlem4  8263  frrlem13  8272  fprlem1  8274  smores2  8318  naddunif  8657  dffi3  9370  marypha1lem  9372  ordtypelem7  9465  ordtypelem8  9466  oismo  9481  unxpwdom2  9529  cantnfres  9625  oemapvali  9632  frmin  9700  frrlem15  9708  frrlem16  9709  tskwe  9901  acndom2  10003  dfac2a  10079  dfac12lem2  10094  cfle  10203  cofsmo  10219  coftr  10223  isf34lem5  10328  isf34lem7  10329  isf34lem6  10330  enfin1ai  10334  fin1a2lem12  10361  ttukeylem7  10465  alephexp1  10530  fpwwe2lem12  10593  fpwwe2  10594  canth4  10598  canthwelem  10601  pwfseqlem1  10609  pwfseqlem4  10613  fzossnn0  13689  fsuppmapnn0fiublem  13996  fsuppmapnn0fiub  13997  xptrrel  14986  limsupgle  15494  limsupgre  15498  rlimres  15575  lo1res  15576  lo1resb  15581  rlimresb  15582  o1resb  15583  o1of2  15630  o1rlimmul  15636  isercolllem2  15683  isercoll  15685  climsup  15687  fprodntriv  15962  bitsinvp1  16473  sadcaddlem  16481  sadadd2lem  16483  sadadd3  16485  sadasslem  16494  sadeq  16496  bitsres  16497  smuval2  16506  smupval  16512  smueqlem  16514  smumul  16517  1arith  16953  isstruct2  17175  setscom  17206  ressress  17273  imasvscafn  17557  imasless  17560  mrcssv  17636  isacs1i  17679  mreacs  17680  acsfn  17681  isacs4lem  18566  isacs5lem  18567  mgmhmima  18739  mhmima  18849  cntzmhm  19371  f1omvdconj  19476  f1omvdco2  19478  symgsssg  19497  symggen  19500  efgval  19747  gsumzaddlem  19951  gsumconst  19964  dmdprdd  20031  dprdfeq0  20054  dprdres  20060  dprdss  20061  dprdz  20062  subgdmdprd  20066  dprddisj2  20071  dprd2dlem1  20073  dprd2da  20074  dprd2d2  20076  dmdprdsplit2lem  20077  gsumle  20175  lmhmlsp  21103  lsppratlem4  21207  islbs3  21212  lbsextlem3  21217  znleval  21593  evpmss  21625  frlmsslsp  21835  lindff1  21859  lindfrn  21860  f1lindf  21861  lindfmm  21866  lsslindf  21869  mplcoe5  22080  mplind  22110  basdif0  23000  tgcl  23016  ppttop  23054  epttop  23056  ntrin  23108  mretopd  23139  neiptoptop  23178  cnclsi  23319  cnconst2  23330  cnrest2  23333  cnpresti  23335  cnprest2  23337  fiuncmp  23451  connsub  23468  connima  23472  iunconnlem  23474  1stcfb  23492  2ndc1stc  23498  2ndcdisj  23503  kgentopon  23585  llycmpkgen2  23597  1stckgenlem  23600  kgencn3  23605  ptclsg  23662  ptcnplem  23668  txtube  23687  hausdiag  23692  txkgen  23699  xkoco1cn  23704  xkoco2cn  23705  xkococnlem  23706  qtoptop2  23746  basqtop  23758  imastopn  23767  hmeores  23818  hmphdis  23843  ptcmpfi  23860  fbssfi  23884  filin  23901  infil  23910  fgtr  23937  elfm  23994  hausflim  24028  flimclslem  24031  fclscmp  24077  cnextcn  24114  tmdgsum2  24143  tgpconncomp  24160  ustexsym  24263  ustund  24269  ustimasn  24275  utoptop  24281  utopbas  24282  restutopopn  24285  blin2  24476  metustexhalf  24603  icccmplem2  24871  icccmplem3  24872  reconnlem2  24875  tcphcph  25286  fmcfil  25321  resscdrg  25407  ivthlem2  25501  ivthlem3  25502  ivth2  25504  ovolfiniun  25550  ovoliunlem1  25551  ismbl2  25576  nulmbl2  25585  unmbl  25586  shftmbl  25587  voliunlem1  25599  voliunlem2  25600  ioombl1lem4  25610  uniioombllem4  25635  uniioombllem5  25636  dyadmbllem  25648  dyadmbl  25649  mbflimsup  25715  i1fima  25727  i1fima2  25728  i1fadd  25744  itg1addlem4  25748  itg2splitlem  25797  itg2split  25798  ellimc3  25928  limcflflem  25929  limcflf  25930  limcresi  25934  limciun  25943  dvreslem  25958  dvres2lem  25959  dvres  25960  dvaddbr  25987  dvmulbr  25988  dvlip  26042  dvlip2  26044  c1liplem1  26045  dvivthlem1  26057  dvne0  26060  lhop1lem  26062  lhop  26065  dvcnvrelem1  26066  dvcnvrelem2  26067  dvfsumle  26070  dvfsumabs  26072  dvfsumlem2  26076  itgsubstlem  26097  mdegleb  26111  mdeglt  26112  mdegldg  26113  mdegxrcl  26114  mdegcl  26116  ig1peu  26222  reeff1olem  26496  logccv  26715  rlimcnp2  27018  lgamgulmlem2  27081  ppisval  27155  prmdvdsfi  27158  mumul  27232  sqff1o  27233  chtlepsi  27257  chpub  27271  dchrisum0lem2a  27568  pntlem3  27660  nosupno  27754  noetalem1  27792  cutlt  28012  negsproplem2  28109  onsbnd  28361  ex-res  30599  htthlem  31076  chlejb1i  31635  ssmd2  32471  fz2ssnn0  32947  gsumpart  33203  gsumhashmul  33207  elrgspnsubrunlem2  33389  extvfvcl  33793  mplvrpmrhm  33804  esplyind  33832  vietalem  33836  locfinreflem  34097  sibfof  34597  sitgclbn  34600  sitgaddlemb  34605  eulerpartlemgu  34634  ballotlemsima  34773  reprinrn  34872  bnj1311  35279  fnrelpredd  35347  erdsze2lem2  35514  iccllysconn  35560  cvmopnlem  35588  msrf  35852  neiin  36652  neibastop1  36679  neibastop2lem  36680  topmeet  36684  ttciunun  36831  poimirlem1  38080  poimirlem2  38081  poimirlem3  38082  poimirlem11  38090  poimirlem12  38091  poimirlem16  38095  poimirlem19  38098  poimirlem30  38109  cnambfre  38127  itg2gt0cn  38134  sstotbnd2  38233  sstotbnd3  38235  ssbnd  38247  ismtyima  38262  heibor1lem  38268  idresssidinxp  38773  pmodlem2  40431  pmodN  40434  diaintclN  41642  djaclN  41720  dibintclN  41751  dicval  41760  dihoml4c  41960  djhcl  41984  infdesc  43185  isnacs2  43247  isnacs3  43251  diophrw  43300  pellfundre  43418  pellfundge  43419  pellfundlb  43421  pellfundglb  43422  fnwe2lem2  43588  lmhmfgima  43621  hbt  43667  omabs2  43869  nadd2rabord  43922  nadd1rabord  43926  cnvtrcl0  44162  trclrelexplem  44247  relexp0a  44252  isotone2  44585  imo72b2lem1  44705  tcfr  45499  modelaxreplem1  45514  wfac8prim  45538  climinf  46142  islptre  46155  limccog  46156  limcleqr  46178  limsupvaluz2  46272  itgcoscmulx  46503  ismbl3  46520  ismbl4  46527  stoweidlem27  46561  dirkercncflem2  46638  fourierdlem38  46679  fourierdlem51  46691  fourierdlem54  46694  fourierdlem63  46703  fourierdlem68  46708  fourierdlem69  46709  fourierdlem70  46710  fourierdlem74  46714  fourierdlem75  46715  fourierdlem76  46716  fourierdlem80  46720  fourierdlem84  46724  fourierdlem85  46725  fourierdlem88  46728  fourierdlem100  46740  fourierdlem101  46741  fourierdlem104  46744  fourierdlem107  46747  fourierdlem111  46751  fourierdlem112  46752  caragenel2d  47066  hoidmv1lelem3  47127  hspmbllem3  47162  sssmf  47272  smfrec  47323  smfsuplem1  47345