Theorem sstrid 3903

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

Syntax hints:   → wi 4   ⊆ wss 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875

This theorem is referenced by:  difsymssdifssd  4158  wereu2  5521  sofld  6016  resssxp  6099  fimass  6540  fvmptss  6771  fimacnv  6830  isofr2  7091  frxp  7825  fnse  7832  smores2  8001  dffi3  8928  marypha1lem  8930  ordtypelem7  9021  ordtypelem8  9022  oismo  9037  unxpwdom2  9085  cantnfres  9173  oemapvali  9180  tskwe  9412  acndom2  9514  dfac2a  9589  dfac12lem2  9604  cfle  9714  cofsmo  9729  coftr  9733  isf34lem5  9838  isf34lem7  9839  isf34lem6  9840  enfin1ai  9844  fin1a2lem12  9871  ttukeylem7  9975  alephexp1  10039  fpwwe2lem12  10102  fpwwe2  10103  canth4  10107  canthwelem  10110  pwfseqlem1  10118  pwfseqlem4  10122  fzossnn0  13117  fsuppmapnn0fiublem  13407  fsuppmapnn0fiub  13408  xptrrel  14387  limsupgle  14882  limsupgre  14886  rlimres  14963  lo1res  14964  lo1resb  14969  rlimresb  14970  o1resb  14971  o1of2  15017  o1rlimmul  15023  isercolllem2  15070  isercoll  15072  climsup  15074  fprodntriv  15344  bitsinvp1  15848  sadcaddlem  15856  sadadd2lem  15858  sadadd3  15860  sadasslem  15869  sadeq  15871  bitsres  15872  smuval2  15881  smupval  15887  smueqlem  15889  smumul  15892  1arith  16318  isstruct2  16551  setscom  16585  ressress  16620  imasvscafn  16868  imasless  16871  mrcssv  16943  isacs1i  16986  mreacs  16987  acsfn  16988  isacs4lem  17844  isacs5lem  17845  mhmima  18055  cntzmhm  18536  f1omvdconj  18641  f1omvdco2  18643  symgsssg  18662  symggen  18665  efgval  18910  gsumzaddlem  19109  gsumconst  19122  dmdprdd  19189  dprdfeq0  19212  dprdres  19218  dprdss  19219  dprdz  19220  subgdmdprd  19224  dprddisj2  19229  dprd2dlem1  19231  dprd2da  19232  dprd2d2  19234  dmdprdsplit2lem  19235  lmhmlsp  19889  lsppratlem4  19990  islbs3  19995  lbsextlem3  20000  znleval  20322  evpmss  20351  frlmsslsp  20561  lindff1  20585  lindfrn  20586  f1lindf  20587  lindfmm  20592  lsslindf  20595  mplcoe5  20800  mplind  20831  basdif0  21653  tgcl  21669  ppttop  21707  epttop  21709  ntrin  21761  mretopd  21792  neiptoptop  21831  cnclsi  21972  cnconst2  21983  cnrest2  21986  cnpresti  21988  cnprest2  21990  fiuncmp  22104  connsub  22121  connima  22125  iunconnlem  22127  1stcfb  22145  2ndc1stc  22151  2ndcdisj  22156  kgentopon  22238  llycmpkgen2  22250  1stckgenlem  22253  kgencn3  22258  ptclsg  22315  ptcnplem  22321  txtube  22340  hausdiag  22345  txkgen  22352  xkoco1cn  22357  xkoco2cn  22358  xkococnlem  22359  qtoptop2  22399  basqtop  22411  imastopn  22420  hmeores  22471  hmphdis  22496  ptcmpfi  22513  fbssfi  22537  filin  22554  infil  22563  fgtr  22590  elfm  22647  hausflim  22681  flimclslem  22684  fclscmp  22730  cnextcn  22767  tmdgsum2  22796  tgpconncomp  22813  ustexsym  22916  ustund  22922  ustimasn  22929  utoptop  22935  utopbas  22936  restutopopn  22939  blin2  23131  metustexhalf  23258  icccmplem2  23524  icccmplem3  23525  reconnlem2  23528  tcphcph  23937  fmcfil  23972  resscdrg  24058  ivthlem2  24152  ivthlem3  24153  ivth2  24155  ovolfiniun  24201  ovoliunlem1  24202  ismbl2  24227  nulmbl2  24236  unmbl  24237  shftmbl  24238  voliunlem1  24250  voliunlem2  24251  ioombl1lem4  24261  uniioombllem4  24286  uniioombllem5  24287  dyadmbllem  24299  dyadmbl  24300  mbflimsup  24366  i1fima  24378  i1fima2  24379  i1fadd  24395  itg1addlem4  24399  itg2splitlem  24448  itg2split  24449  ellimc3  24578  limcflflem  24579  limcflf  24580  limcresi  24584  limciun  24593  dvreslem  24608  dvres2lem  24609  dvres  24610  dvaddbr  24637  dvmulbr  24638  dvlip  24692  dvlip2  24694  c1liplem1  24695  dvivthlem1  24707  dvne0  24710  lhop1lem  24712  lhop  24715  dvcnvrelem1  24716  dvcnvrelem2  24717  dvfsumle  24720  dvfsumabs  24722  dvfsumlem2  24726  itgsubstlem  24747  mdegleb  24764  mdeglt  24765  mdegldg  24766  mdegxrcl  24767  mdegcl  24769  ig1peu  24871  reeff1olem  25140  logccv  25353  rlimcnp2  25651  lgamgulmlem2  25714  ppisval  25788  prmdvdsfi  25791  mumul  25865  sqff1o  25866  chtlepsi  25889  chpub  25903  dchrisum0lem2a  26200  pntlem3  26292  ex-res  28325  htthlem  28799  chlejb1i  29358  ssmd2  30194  fz2ssnn0  30630  gsumpart  30841  gsumhashmul  30842  gsumle  30876  locfinreflem  31311  sibfof  31826  sitgclbn  31829  sitgaddlemb  31834  eulerpartlemgu  31863  ballotlemsima  32001  reprinrn  32117  bnj1311  32524  fnrelpredd  32590  erdsze2lem2  32682  iccllysconn  32728  cvmopnlem  32756  msrf  33020  frpomin  33325  frxp2  33346  frxp3  33352  frrlem4  33387  frrlem13  33396  fprlem1  33398  frrlem15  33403  nosupno  33471  noetalem1  33509  neiin  34070  neibastop1  34097  neibastop2lem  34098  topmeet  34102  poimirlem1  35338  poimirlem2  35339  poimirlem3  35340  poimirlem11  35348  poimirlem12  35349  poimirlem16  35353  poimirlem19  35356  poimirlem30  35367  cnambfre  35385  itg2gt0cn  35392  sstotbnd2  35492  sstotbnd3  35494  ssbnd  35506  ismtyima  35521  heibor1lem  35527  idresssidinxp  36006  pmodlem2  37423  pmodN  37426  diaintclN  38634  djaclN  38712  dibintclN  38743  dicval  38752  dihoml4c  38952  djhcl  38976  infdesc  39972  isnacs2  40020  isnacs3  40024  diophrw  40073  pellfundre  40195  pellfundge  40196  pellfundlb  40198  pellfundglb  40199  fnwe2lem2  40368  lmhmfgima  40401  hbt  40447  cnvtrcl0  40699  trclrelexplem  40785  relexp0a  40790  isotone2  41125  imo72b2lem1  41247  climinf  42614  islptre  42627  limccog  42628  limcleqr  42652  itgcoscmulx  42977  ismbl3  42994  ismbl4  43001  stoweidlem27  43035  dirkercncflem2  43112  fourierdlem38  43153  fourierdlem49  43163  fourierdlem51  43165  fourierdlem54  43168  fourierdlem63  43177  fourierdlem68  43182  fourierdlem69  43183  fourierdlem70  43184  fourierdlem74  43188  fourierdlem75  43189  fourierdlem76  43190  fourierdlem80  43194  fourierdlem84  43198  fourierdlem85  43199  fourierdlem88  43202  fourierdlem100  43214  fourierdlem101  43215  fourierdlem104  43218  fourierdlem107  43221  fourierdlem111  43225  fourierdlem112  43226  caragenel2d  43537  hoidmv1lelem3  43598  hspmbllem3  43633  sssmf  43738  smfrec  43787  smfsuplem1  43808  mgmhmima  44789