Theorem sstrid 3949

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

Syntax hints:   → wi 4   ⊆ wss 3905

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

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

This theorem is referenced by:  difsymssdifssd  4217  wereu2  5620  sofld  6140  resssxp  6222  frpomin  6292  fimass  6676  fvmptss  6946  isofr2  7285  frxp  8066  fnse  8073  frxp2  8084  frxp3  8091  frrlem4  8229  frrlem13  8238  fprlem1  8240  smores2  8284  naddunif  8618  dffi3  9340  marypha1lem  9342  ordtypelem7  9435  ordtypelem8  9436  oismo  9451  unxpwdom2  9499  cantnfres  9592  oemapvali  9599  frmin  9664  frrlem15  9672  frrlem16  9673  tskwe  9865  acndom2  9967  dfac2a  10043  dfac12lem2  10058  cfle  10167  cofsmo  10182  coftr  10186  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  enfin1ai  10297  fin1a2lem12  10324  ttukeylem7  10428  alephexp1  10492  fpwwe2lem12  10555  fpwwe2  10556  canth4  10560  canthwelem  10563  pwfseqlem1  10571  pwfseqlem4  10575  fzossnn0  13611  fsuppmapnn0fiublem  13915  fsuppmapnn0fiub  13916  xptrrel  14905  limsupgle  15402  limsupgre  15406  rlimres  15483  lo1res  15484  lo1resb  15489  rlimresb  15490  o1resb  15491  o1of2  15538  o1rlimmul  15544  isercolllem2  15591  isercoll  15593  climsup  15595  fprodntriv  15867  bitsinvp1  16378  sadcaddlem  16386  sadadd2lem  16388  sadadd3  16390  sadasslem  16399  sadeq  16401  bitsres  16402  smuval2  16411  smupval  16417  smueqlem  16419  smumul  16422  1arith  16857  isstruct2  17078  setscom  17109  ressress  17176  imasvscafn  17459  imasless  17462  mrcssv  17538  isacs1i  17581  mreacs  17582  acsfn  17583  isacs4lem  18468  isacs5lem  18469  mgmhmima  18607  mhmima  18717  cntzmhm  19238  f1omvdconj  19343  f1omvdco2  19345  symgsssg  19364  symggen  19367  efgval  19614  gsumzaddlem  19818  gsumconst  19831  dmdprdd  19898  dprdfeq0  19921  dprdres  19927  dprdss  19928  dprdz  19929  subgdmdprd  19933  dprddisj2  19938  dprd2dlem1  19940  dprd2da  19941  dprd2d2  19943  dmdprdsplit2lem  19944  gsumle  20042  lmhmlsp  20971  lsppratlem4  21075  islbs3  21080  lbsextlem3  21085  znleval  21479  evpmss  21511  frlmsslsp  21721  lindff1  21745  lindfrn  21746  f1lindf  21747  lindfmm  21752  lsslindf  21755  mplcoe5  21963  mplind  21993  basdif0  22856  tgcl  22872  ppttop  22910  epttop  22912  ntrin  22964  mretopd  22995  neiptoptop  23034  cnclsi  23175  cnconst2  23186  cnrest2  23189  cnpresti  23191  cnprest2  23193  fiuncmp  23307  connsub  23324  connima  23328  iunconnlem  23330  1stcfb  23348  2ndc1stc  23354  2ndcdisj  23359  kgentopon  23441  llycmpkgen2  23453  1stckgenlem  23456  kgencn3  23461  ptclsg  23518  ptcnplem  23524  txtube  23543  hausdiag  23548  txkgen  23555  xkoco1cn  23560  xkoco2cn  23561  xkococnlem  23562  qtoptop2  23602  basqtop  23614  imastopn  23623  hmeores  23674  hmphdis  23699  ptcmpfi  23716  fbssfi  23740  filin  23757  infil  23766  fgtr  23793  elfm  23850  hausflim  23884  flimclslem  23887  fclscmp  23933  cnextcn  23970  tmdgsum2  23999  tgpconncomp  24016  ustexsym  24119  ustund  24125  ustimasn  24132  utoptop  24138  utopbas  24139  restutopopn  24142  blin2  24333  metustexhalf  24460  icccmplem2  24728  icccmplem3  24729  reconnlem2  24732  tcphcph  25153  fmcfil  25188  resscdrg  25274  ivthlem2  25369  ivthlem3  25370  ivth2  25372  ovolfiniun  25418  ovoliunlem1  25419  ismbl2  25444  nulmbl2  25453  unmbl  25454  shftmbl  25455  voliunlem1  25467  voliunlem2  25468  ioombl1lem4  25478  uniioombllem4  25503  uniioombllem5  25504  dyadmbllem  25516  dyadmbl  25517  mbflimsup  25583  i1fima  25595  i1fima2  25596  i1fadd  25612  itg1addlem4  25616  itg2splitlem  25665  itg2split  25666  ellimc3  25796  limcflflem  25797  limcflf  25798  limcresi  25802  limciun  25811  dvreslem  25826  dvres2lem  25827  dvres  25828  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvlip  25914  dvlip2  25916  c1liplem1  25917  dvivthlem1  25929  dvne0  25932  lhop1lem  25934  lhop  25937  dvcnvrelem1  25938  dvcnvrelem2  25939  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  itgsubstlem  25971  mdegleb  25985  mdeglt  25986  mdegldg  25987  mdegxrcl  25988  mdegcl  25990  ig1peu  26096  reeff1olem  26372  logccv  26588  rlimcnp2  26892  lgamgulmlem2  26956  ppisval  27030  prmdvdsfi  27033  mumul  27107  sqff1o  27108  chtlepsi  27133  chpub  27147  dchrisum0lem2a  27444  pntlem3  27536  nosupno  27631  noetalem1  27669  cutlt  27863  negsproplem2  27958  ex-res  30403  htthlem  30879  chlejb1i  31438  ssmd2  32274  fz2ssnn0  32741  gsumpart  33023  gsumhashmul  33027  elrgspnsubrunlem2  33201  locfinreflem  33809  sibfof  34310  sitgclbn  34313  sitgaddlemb  34318  eulerpartlemgu  34347  ballotlemsima  34486  reprinrn  34588  bnj1311  34993  fnrelpredd  35058  erdsze2lem2  35179  iccllysconn  35225  cvmopnlem  35253  msrf  35517  neiin  36308  neibastop1  36335  neibastop2lem  36336  topmeet  36340  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem11  37613  poimirlem12  37614  poimirlem16  37618  poimirlem19  37621  poimirlem30  37632  cnambfre  37650  itg2gt0cn  37657  sstotbnd2  37756  sstotbnd3  37758  ssbnd  37770  ismtyima  37785  heibor1lem  37791  idresssidinxp  38284  pmodlem2  39829  pmodN  39832  diaintclN  41040  djaclN  41118  dibintclN  41149  dicval  41158  dihoml4c  41358  djhcl  41382  infdesc  42619  isnacs2  42682  isnacs3  42686  diophrw  42735  pellfundre  42857  pellfundge  42858  pellfundlb  42860  pellfundglb  42861  fnwe2lem2  43027  lmhmfgima  43060  hbt  43106  omabs2  43308  nadd2rabord  43361  nadd1rabord  43365  cnvtrcl0  43602  trclrelexplem  43687  relexp0a  43692  isotone2  44025  imo72b2lem1  44145  tcfr  44940  modelaxreplem1  44955  wfac8prim  44979  climinf  45591  islptre  45604  limccog  45605  limcleqr  45629  limsupvaluz2  45723  itgcoscmulx  45954  ismbl3  45971  ismbl4  45978  stoweidlem27  46012  dirkercncflem2  46089  fourierdlem38  46130  fourierdlem49  46140  fourierdlem51  46142  fourierdlem54  46145  fourierdlem63  46154  fourierdlem68  46159  fourierdlem69  46160  fourierdlem70  46161  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem80  46171  fourierdlem84  46175  fourierdlem85  46176  fourierdlem88  46179  fourierdlem100  46191  fourierdlem101  46192  fourierdlem104  46195  fourierdlem107  46198  fourierdlem111  46202  fourierdlem112  46203  caragenel2d  46517  hoidmv1lelem3  46578  hspmbllem3  46613  sssmf  46723  smfrec  46774  smfsuplem1  46796