Theorem sstrid 3970

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

Syntax hints:   → wi 4   ⊆ wss 3926

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 3943

This theorem is referenced by:  difsymssdifssd  4239  wereu2  5651  sofld  6176  resssxp  6259  frpomin  6329  fimass  6725  fvmptss  6997  isofr2  7336  frxp  8123  fnse  8130  frxp2  8141  frxp3  8148  frrlem4  8286  frrlem13  8295  fprlem1  8297  smores2  8366  naddunif  8703  dffi3  9441  marypha1lem  9443  ordtypelem7  9536  ordtypelem8  9537  oismo  9552  unxpwdom2  9600  cantnfres  9689  oemapvali  9696  frmin  9761  frrlem15  9769  frrlem16  9770  tskwe  9962  acndom2  10066  dfac2a  10142  dfac12lem2  10157  cfle  10266  cofsmo  10281  coftr  10285  isf34lem5  10390  isf34lem7  10391  isf34lem6  10392  enfin1ai  10396  fin1a2lem12  10423  ttukeylem7  10527  alephexp1  10591  fpwwe2lem12  10654  fpwwe2  10655  canth4  10659  canthwelem  10662  pwfseqlem1  10670  pwfseqlem4  10674  fzossnn0  13705  fsuppmapnn0fiublem  14006  fsuppmapnn0fiub  14007  xptrrel  14997  limsupgle  15491  limsupgre  15495  rlimres  15572  lo1res  15573  lo1resb  15578  rlimresb  15579  o1resb  15580  o1of2  15627  o1rlimmul  15633  isercolllem2  15680  isercoll  15682  climsup  15684  fprodntriv  15956  bitsinvp1  16466  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadasslem  16487  sadeq  16489  bitsres  16490  smuval2  16499  smupval  16505  smueqlem  16507  smumul  16510  1arith  16945  isstruct2  17166  setscom  17197  ressress  17266  imasvscafn  17549  imasless  17552  mrcssv  17624  isacs1i  17667  mreacs  17668  acsfn  17669  isacs4lem  18552  isacs5lem  18553  mgmhmima  18691  mhmima  18801  cntzmhm  19322  f1omvdconj  19425  f1omvdco2  19427  symgsssg  19446  symggen  19449  efgval  19696  gsumzaddlem  19900  gsumconst  19913  dmdprdd  19980  dprdfeq0  20003  dprdres  20009  dprdss  20010  dprdz  20011  subgdmdprd  20015  dprddisj2  20020  dprd2dlem1  20022  dprd2da  20023  dprd2d2  20025  dmdprdsplit2lem  20026  lmhmlsp  21005  lsppratlem4  21109  islbs3  21114  lbsextlem3  21119  znleval  21513  evpmss  21544  frlmsslsp  21754  lindff1  21778  lindfrn  21779  f1lindf  21780  lindfmm  21785  lsslindf  21788  mplcoe5  21996  mplind  22026  basdif0  22889  tgcl  22905  ppttop  22943  epttop  22945  ntrin  22997  mretopd  23028  neiptoptop  23067  cnclsi  23208  cnconst2  23219  cnrest2  23222  cnpresti  23224  cnprest2  23226  fiuncmp  23340  connsub  23357  connima  23361  iunconnlem  23363  1stcfb  23381  2ndc1stc  23387  2ndcdisj  23392  kgentopon  23474  llycmpkgen2  23486  1stckgenlem  23489  kgencn3  23494  ptclsg  23551  ptcnplem  23557  txtube  23576  hausdiag  23581  txkgen  23588  xkoco1cn  23593  xkoco2cn  23594  xkococnlem  23595  qtoptop2  23635  basqtop  23647  imastopn  23656  hmeores  23707  hmphdis  23732  ptcmpfi  23749  fbssfi  23773  filin  23790  infil  23799  fgtr  23826  elfm  23883  hausflim  23917  flimclslem  23920  fclscmp  23966  cnextcn  24003  tmdgsum2  24032  tgpconncomp  24049  ustexsym  24152  ustund  24158  ustimasn  24165  utoptop  24171  utopbas  24172  restutopopn  24175  blin2  24366  metustexhalf  24493  icccmplem2  24761  icccmplem3  24762  reconnlem2  24765  tcphcph  25187  fmcfil  25222  resscdrg  25308  ivthlem2  25403  ivthlem3  25404  ivth2  25406  ovolfiniun  25452  ovoliunlem1  25453  ismbl2  25478  nulmbl2  25487  unmbl  25488  shftmbl  25489  voliunlem1  25501  voliunlem2  25502  ioombl1lem4  25512  uniioombllem4  25537  uniioombllem5  25538  dyadmbllem  25550  dyadmbl  25551  mbflimsup  25617  i1fima  25629  i1fima2  25630  i1fadd  25646  itg1addlem4  25650  itg2splitlem  25699  itg2split  25700  ellimc3  25830  limcflflem  25831  limcflf  25832  limcresi  25836  limciun  25845  dvreslem  25860  dvres2lem  25861  dvres  25862  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvlip  25948  dvlip2  25950  c1liplem1  25951  dvivthlem1  25963  dvne0  25966  lhop1lem  25968  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubstlem  26005  mdegleb  26019  mdeglt  26020  mdegldg  26021  mdegxrcl  26022  mdegcl  26024  ig1peu  26130  reeff1olem  26406  logccv  26622  rlimcnp2  26926  lgamgulmlem2  26990  ppisval  27064  prmdvdsfi  27067  mumul  27141  sqff1o  27142  chtlepsi  27167  chpub  27181  dchrisum0lem2a  27478  pntlem3  27570  nosupno  27665  noetalem1  27703  cutlt  27883  negsproplem2  27978  ex-res  30368  htthlem  30844  chlejb1i  31403  ssmd2  32239  fz2ssnn0  32708  gsumpart  32997  gsumhashmul  33001  gsumle  33038  elrgspnsubrunlem2  33189  locfinreflem  33817  sibfof  34318  sitgclbn  34321  sitgaddlemb  34326  eulerpartlemgu  34355  ballotlemsima  34494  reprinrn  34596  bnj1311  35001  fnrelpredd  35066  erdsze2lem2  35172  iccllysconn  35218  cvmopnlem  35246  msrf  35510  neiin  36296  neibastop1  36323  neibastop2lem  36324  topmeet  36328  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem19  37609  poimirlem30  37620  cnambfre  37638  itg2gt0cn  37645  sstotbnd2  37744  sstotbnd3  37746  ssbnd  37758  ismtyima  37773  heibor1lem  37779  idresssidinxp  38272  pmodlem2  39812  pmodN  39815  diaintclN  41023  djaclN  41101  dibintclN  41132  dicval  41141  dihoml4c  41341  djhcl  41365  infdesc  42613  isnacs2  42676  isnacs3  42680  diophrw  42729  pellfundre  42851  pellfundge  42852  pellfundlb  42854  pellfundglb  42855  fnwe2lem2  43022  lmhmfgima  43055  hbt  43101  omabs2  43303  nadd2rabord  43356  nadd1rabord  43360  cnvtrcl0  43597  trclrelexplem  43682  relexp0a  43687  isotone2  44020  imo72b2lem1  44140  tcfr  44936  modelaxreplem1  44951  wfac8prim  44975  climinf  45583  islptre  45596  limccog  45597  limcleqr  45621  limsupvaluz2  45715  itgcoscmulx  45946  ismbl3  45963  ismbl4  45970  stoweidlem27  46004  dirkercncflem2  46081  fourierdlem38  46122  fourierdlem49  46132  fourierdlem51  46134  fourierdlem54  46137  fourierdlem63  46146  fourierdlem68  46151  fourierdlem69  46152  fourierdlem70  46153  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem80  46163  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem100  46183  fourierdlem101  46184  fourierdlem104  46187  fourierdlem107  46190  fourierdlem111  46194  fourierdlem112  46195  caragenel2d  46509  hoidmv1lelem3  46570  hspmbllem3  46605  sssmf  46715  smfrec  46766  smfsuplem1  46788