Theorem sstrid 3961

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

Syntax hints:   → wi 4   ⊆ wss 3917

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 3934

This theorem is referenced by:  difsymssdifssd  4230  wereu2  5638  sofld  6163  resssxp  6246  frpomin  6316  fimass  6711  fvmptss  6983  isofr2  7322  frxp  8108  fnse  8115  frxp2  8126  frxp3  8133  frrlem4  8271  frrlem13  8280  fprlem1  8282  smores2  8326  naddunif  8660  dffi3  9389  marypha1lem  9391  ordtypelem7  9484  ordtypelem8  9485  oismo  9500  unxpwdom2  9548  cantnfres  9637  oemapvali  9644  frmin  9709  frrlem15  9717  frrlem16  9718  tskwe  9910  acndom2  10014  dfac2a  10090  dfac12lem2  10105  cfle  10214  cofsmo  10229  coftr  10233  isf34lem5  10338  isf34lem7  10339  isf34lem6  10340  enfin1ai  10344  fin1a2lem12  10371  ttukeylem7  10475  alephexp1  10539  fpwwe2lem12  10602  fpwwe2  10603  canth4  10607  canthwelem  10610  pwfseqlem1  10618  pwfseqlem4  10622  fzossnn0  13658  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  xptrrel  14953  limsupgle  15450  limsupgre  15454  rlimres  15531  lo1res  15532  lo1resb  15537  rlimresb  15538  o1resb  15539  o1of2  15586  o1rlimmul  15592  isercolllem2  15639  isercoll  15641  climsup  15643  fprodntriv  15915  bitsinvp1  16426  sadcaddlem  16434  sadadd2lem  16436  sadadd3  16438  sadasslem  16447  sadeq  16449  bitsres  16450  smuval2  16459  smupval  16465  smueqlem  16467  smumul  16470  1arith  16905  isstruct2  17126  setscom  17157  ressress  17224  imasvscafn  17507  imasless  17510  mrcssv  17582  isacs1i  17625  mreacs  17626  acsfn  17627  isacs4lem  18510  isacs5lem  18511  mgmhmima  18649  mhmima  18759  cntzmhm  19280  f1omvdconj  19383  f1omvdco2  19385  symgsssg  19404  symggen  19407  efgval  19654  gsumzaddlem  19858  gsumconst  19871  dmdprdd  19938  dprdfeq0  19961  dprdres  19967  dprdss  19968  dprdz  19969  subgdmdprd  19973  dprddisj2  19978  dprd2dlem1  19980  dprd2da  19981  dprd2d2  19983  dmdprdsplit2lem  19984  lmhmlsp  20963  lsppratlem4  21067  islbs3  21072  lbsextlem3  21077  znleval  21471  evpmss  21502  frlmsslsp  21712  lindff1  21736  lindfrn  21737  f1lindf  21738  lindfmm  21743  lsslindf  21746  mplcoe5  21954  mplind  21984  basdif0  22847  tgcl  22863  ppttop  22901  epttop  22903  ntrin  22955  mretopd  22986  neiptoptop  23025  cnclsi  23166  cnconst2  23177  cnrest2  23180  cnpresti  23182  cnprest2  23184  fiuncmp  23298  connsub  23315  connima  23319  iunconnlem  23321  1stcfb  23339  2ndc1stc  23345  2ndcdisj  23350  kgentopon  23432  llycmpkgen2  23444  1stckgenlem  23447  kgencn3  23452  ptclsg  23509  ptcnplem  23515  txtube  23534  hausdiag  23539  txkgen  23546  xkoco1cn  23551  xkoco2cn  23552  xkococnlem  23553  qtoptop2  23593  basqtop  23605  imastopn  23614  hmeores  23665  hmphdis  23690  ptcmpfi  23707  fbssfi  23731  filin  23748  infil  23757  fgtr  23784  elfm  23841  hausflim  23875  flimclslem  23878  fclscmp  23924  cnextcn  23961  tmdgsum2  23990  tgpconncomp  24007  ustexsym  24110  ustund  24116  ustimasn  24123  utoptop  24129  utopbas  24130  restutopopn  24133  blin2  24324  metustexhalf  24451  icccmplem2  24719  icccmplem3  24720  reconnlem2  24723  tcphcph  25144  fmcfil  25179  resscdrg  25265  ivthlem2  25360  ivthlem3  25361  ivth2  25363  ovolfiniun  25409  ovoliunlem1  25410  ismbl2  25435  nulmbl2  25444  unmbl  25445  shftmbl  25446  voliunlem1  25458  voliunlem2  25459  ioombl1lem4  25469  uniioombllem4  25494  uniioombllem5  25495  dyadmbllem  25507  dyadmbl  25508  mbflimsup  25574  i1fima  25586  i1fima2  25587  i1fadd  25603  itg1addlem4  25607  itg2splitlem  25656  itg2split  25657  ellimc3  25787  limcflflem  25788  limcflf  25789  limcresi  25793  limciun  25802  dvreslem  25817  dvres2lem  25818  dvres  25819  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvlip  25905  dvlip2  25907  c1liplem1  25908  dvivthlem1  25920  dvne0  25923  lhop1lem  25925  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubstlem  25962  mdegleb  25976  mdeglt  25977  mdegldg  25978  mdegxrcl  25979  mdegcl  25981  ig1peu  26087  reeff1olem  26363  logccv  26579  rlimcnp2  26883  lgamgulmlem2  26947  ppisval  27021  prmdvdsfi  27024  mumul  27098  sqff1o  27099  chtlepsi  27124  chpub  27138  dchrisum0lem2a  27435  pntlem3  27527  nosupno  27622  noetalem1  27660  cutlt  27847  negsproplem2  27942  ex-res  30377  htthlem  30853  chlejb1i  31412  ssmd2  32248  fz2ssnn0  32715  gsumpart  33004  gsumhashmul  33008  gsumle  33045  elrgspnsubrunlem2  33206  locfinreflem  33837  sibfof  34338  sitgclbn  34341  sitgaddlemb  34346  eulerpartlemgu  34375  ballotlemsima  34514  reprinrn  34616  bnj1311  35021  fnrelpredd  35086  erdsze2lem2  35198  iccllysconn  35244  cvmopnlem  35272  msrf  35536  neiin  36327  neibastop1  36354  neibastop2lem  36355  topmeet  36359  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem19  37640  poimirlem30  37651  cnambfre  37669  itg2gt0cn  37676  sstotbnd2  37775  sstotbnd3  37777  ssbnd  37789  ismtyima  37804  heibor1lem  37810  idresssidinxp  38303  pmodlem2  39848  pmodN  39851  diaintclN  41059  djaclN  41137  dibintclN  41168  dicval  41177  dihoml4c  41377  djhcl  41401  infdesc  42638  isnacs2  42701  isnacs3  42705  diophrw  42754  pellfundre  42876  pellfundge  42877  pellfundlb  42879  pellfundglb  42880  fnwe2lem2  43047  lmhmfgima  43080  hbt  43126  omabs2  43328  nadd2rabord  43381  nadd1rabord  43385  cnvtrcl0  43622  trclrelexplem  43707  relexp0a  43712  isotone2  44045  imo72b2lem1  44165  tcfr  44960  modelaxreplem1  44975  wfac8prim  44999  climinf  45611  islptre  45624  limccog  45625  limcleqr  45649  limsupvaluz2  45743  itgcoscmulx  45974  ismbl3  45991  ismbl4  45998  stoweidlem27  46032  dirkercncflem2  46109  fourierdlem38  46150  fourierdlem49  46160  fourierdlem51  46162  fourierdlem54  46165  fourierdlem63  46174  fourierdlem68  46179  fourierdlem69  46180  fourierdlem70  46181  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem80  46191  fourierdlem84  46195  fourierdlem85  46196  fourierdlem88  46199  fourierdlem100  46211  fourierdlem101  46212  fourierdlem104  46215  fourierdlem107  46218  fourierdlem111  46222  fourierdlem112  46223  caragenel2d  46537  hoidmv1lelem3  46598  hspmbllem3  46633  sssmf  46743  smfrec  46794  smfsuplem1  46816