Theorem sstrid 3934

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

Syntax hints:   → wi 4   ⊆ wss 3890

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 3907

This theorem is referenced by:  difsymssdifssd  4205  wereu2  5619  sofld  6143  resssxp  6226  frpomin  6296  fimass  6680  fvmptss  6952  isofr2  7290  frxp  8067  fnse  8074  frxp2  8085  frxp3  8092  frrlem4  8230  frrlem13  8239  fprlem1  8241  smores2  8285  naddunif  8620  dffi3  9335  marypha1lem  9337  ordtypelem7  9430  ordtypelem8  9431  oismo  9446  unxpwdom2  9494  cantnfres  9587  oemapvali  9594  frmin  9662  frrlem15  9670  frrlem16  9671  tskwe  9863  acndom2  9965  dfac2a  10041  dfac12lem2  10056  cfle  10165  cofsmo  10180  coftr  10184  isf34lem5  10289  isf34lem7  10290  isf34lem6  10291  enfin1ai  10295  fin1a2lem12  10322  ttukeylem7  10426  alephexp1  10491  fpwwe2lem12  10554  fpwwe2  10555  canth4  10559  canthwelem  10562  pwfseqlem1  10570  pwfseqlem4  10574  fzossnn0  13607  fsuppmapnn0fiublem  13914  fsuppmapnn0fiub  13915  xptrrel  14904  limsupgle  15401  limsupgre  15405  rlimres  15482  lo1res  15483  lo1resb  15488  rlimresb  15489  o1resb  15490  o1of2  15537  o1rlimmul  15543  isercolllem2  15590  isercoll  15592  climsup  15594  fprodntriv  15866  bitsinvp1  16377  sadcaddlem  16385  sadadd2lem  16387  sadadd3  16389  sadasslem  16398  sadeq  16400  bitsres  16401  smuval2  16410  smupval  16416  smueqlem  16418  smumul  16421  1arith  16856  isstruct2  17077  setscom  17108  ressress  17175  imasvscafn  17459  imasless  17462  mrcssv  17538  isacs1i  17581  mreacs  17582  acsfn  17583  isacs4lem  18468  isacs5lem  18469  mgmhmima  18641  mhmima  18751  cntzmhm  19274  f1omvdconj  19379  f1omvdco2  19381  symgsssg  19400  symggen  19403  efgval  19650  gsumzaddlem  19854  gsumconst  19867  dmdprdd  19934  dprdfeq0  19957  dprdres  19963  dprdss  19964  dprdz  19965  subgdmdprd  19969  dprddisj2  19974  dprd2dlem1  19976  dprd2da  19977  dprd2d2  19979  dmdprdsplit2lem  19980  gsumle  20078  lmhmlsp  21003  lsppratlem4  21107  islbs3  21112  lbsextlem3  21117  znleval  21511  evpmss  21543  frlmsslsp  21753  lindff1  21777  lindfrn  21778  f1lindf  21779  lindfmm  21784  lsslindf  21787  mplcoe5  21996  mplind  22026  basdif0  22896  tgcl  22912  ppttop  22950  epttop  22952  ntrin  23004  mretopd  23035  neiptoptop  23074  cnclsi  23215  cnconst2  23226  cnrest2  23229  cnpresti  23231  cnprest2  23233  fiuncmp  23347  connsub  23364  connima  23368  iunconnlem  23370  1stcfb  23388  2ndc1stc  23394  2ndcdisj  23399  kgentopon  23481  llycmpkgen2  23493  1stckgenlem  23496  kgencn3  23501  ptclsg  23558  ptcnplem  23564  txtube  23583  hausdiag  23588  txkgen  23595  xkoco1cn  23600  xkoco2cn  23601  xkococnlem  23602  qtoptop2  23642  basqtop  23654  imastopn  23663  hmeores  23714  hmphdis  23739  ptcmpfi  23756  fbssfi  23780  filin  23797  infil  23806  fgtr  23833  elfm  23890  hausflim  23924  flimclslem  23927  fclscmp  23973  cnextcn  24010  tmdgsum2  24039  tgpconncomp  24056  ustexsym  24159  ustund  24165  ustimasn  24171  utoptop  24177  utopbas  24178  restutopopn  24181  blin2  24372  metustexhalf  24499  icccmplem2  24767  icccmplem3  24768  reconnlem2  24771  tcphcph  25182  fmcfil  25217  resscdrg  25303  ivthlem2  25397  ivthlem3  25398  ivth2  25400  ovolfiniun  25446  ovoliunlem1  25447  ismbl2  25472  nulmbl2  25481  unmbl  25482  shftmbl  25483  voliunlem1  25495  voliunlem2  25496  ioombl1lem4  25506  uniioombllem4  25531  uniioombllem5  25532  dyadmbllem  25544  dyadmbl  25545  mbflimsup  25611  i1fima  25623  i1fima2  25624  i1fadd  25640  itg1addlem4  25644  itg2splitlem  25693  itg2split  25694  ellimc3  25824  limcflflem  25825  limcflf  25826  limcresi  25830  limciun  25839  dvreslem  25854  dvres2lem  25855  dvres  25856  dvaddbr  25883  dvmulbr  25884  dvlip  25939  dvlip2  25941  c1liplem1  25942  dvivthlem1  25954  dvne0  25957  lhop1lem  25959  lhop  25962  dvcnvrelem1  25963  dvcnvrelem2  25964  dvfsumle  25967  dvfsumleOLD  25968  dvfsumabs  25970  dvfsumlem2  25974  dvfsumlem2OLD  25975  itgsubstlem  25996  mdegleb  26010  mdeglt  26011  mdegldg  26012  mdegxrcl  26013  mdegcl  26015  ig1peu  26121  reeff1olem  26396  logccv  26612  rlimcnp2  26916  lgamgulmlem2  26980  ppisval  27054  prmdvdsfi  27057  mumul  27131  sqff1o  27132  chtlepsi  27157  chpub  27171  dchrisum0lem2a  27468  pntlem3  27560  nosupno  27655  noetalem1  27693  cutlt  27912  negsproplem2  28009  onsbnd  28261  ex-res  30500  htthlem  30977  chlejb1i  31536  ssmd2  32372  fz2ssnn0  32848  gsumpart  33129  gsumhashmul  33133  elrgspnsubrunlem2  33314  extvfvcl  33685  mplvrpmrhm  33696  esplyind  33724  vietalem  33728  locfinreflem  33990  sibfof  34490  sitgclbn  34493  sitgaddlemb  34498  eulerpartlemgu  34527  ballotlemsima  34666  reprinrn  34768  bnj1311  35172  fnrelpredd  35240  erdsze2lem2  35392  iccllysconn  35438  cvmopnlem  35466  msrf  35730  neiin  36520  neibastop1  36547  neibastop2lem  36548  topmeet  36552  ttciunun  36699  poimirlem1  37933  poimirlem2  37934  poimirlem3  37935  poimirlem11  37943  poimirlem12  37944  poimirlem16  37948  poimirlem19  37951  poimirlem30  37962  cnambfre  37980  itg2gt0cn  37987  sstotbnd2  38086  sstotbnd3  38088  ssbnd  38100  ismtyima  38115  heibor1lem  38121  idresssidinxp  38626  pmodlem2  40284  pmodN  40287  diaintclN  41495  djaclN  41573  dibintclN  41604  dicval  41613  dihoml4c  41813  djhcl  41837  infdesc  43075  isnacs2  43137  isnacs3  43141  diophrw  43190  pellfundre  43312  pellfundge  43313  pellfundlb  43315  pellfundglb  43316  fnwe2lem2  43482  lmhmfgima  43515  hbt  43561  omabs2  43763  nadd2rabord  43816  nadd1rabord  43820  cnvtrcl0  44056  trclrelexplem  44141  relexp0a  44146  isotone2  44479  imo72b2lem1  44599  tcfr  45393  modelaxreplem1  45408  wfac8prim  45432  climinf  46040  islptre  46053  limccog  46054  limcleqr  46076  limsupvaluz2  46170  itgcoscmulx  46401  ismbl3  46418  ismbl4  46425  stoweidlem27  46459  dirkercncflem2  46536  fourierdlem38  46577  fourierdlem49  46587  fourierdlem51  46589  fourierdlem54  46592  fourierdlem63  46601  fourierdlem68  46606  fourierdlem69  46607  fourierdlem70  46608  fourierdlem74  46612  fourierdlem75  46613  fourierdlem76  46614  fourierdlem80  46618  fourierdlem84  46622  fourierdlem85  46623  fourierdlem88  46626  fourierdlem100  46638  fourierdlem101  46639  fourierdlem104  46642  fourierdlem107  46645  fourierdlem111  46649  fourierdlem112  46650  caragenel2d  46964  hoidmv1lelem3  47025  hspmbllem3  47060  sssmf  47170  smfrec  47221  smfsuplem1  47243