Theorem ssrind 4198

Description: Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Hypothesis

Ref	Expression
ssrind.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssrind	⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Proof of Theorem ssrind

Step	Hyp	Ref	Expression
1		ssrind.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssrin 4196	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∩ cin 3906   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-ss 3924

This theorem is referenced by:  fictb  10215  isacs1i  17703  rescabs  17880  lsmdisj  19742  dmdprdsplit2lem  20108  rhmsscrnghm  20741  rngcresringcat  20745  acsfn1p  20871  obselocv  21838  restbas  23276  neitr  23298  restcls  23299  restntr  23300  nrmsep  23475  cldllycmp  23613  fclsneii  24135  tsmsres  24262  trcfilu  24411  metdseq0  24973  iundisj2  25669  uniioombllem3  25705  ppisval  27226  ppisval2  27227  chtwordi  27278  ppiwordi  27284  chpub  27342  chebbnd1lem1  27591  mdbr2  32557  mdslj1i  32580  mdsl2i  32583  mdslmd1lem1  32586  mdslmd3i  32593  mdexchi  32596  sumdmdlem  32679  iundisj2f  32845  iundisj2fi  33054  cycpmco2f1  33357  tocyccntz  33377  esumrnmpt2  34375  bnj1177  35311  sstotbnd2  38285  lcvexchlem5  39674  pnonsingN  40569  dochnoncon  42027  eldioph2lem2  43354  limsupres  46277  limsupresxr  46338  liminfresxr  46339  liminflelimsuplem  46347  ssdisjd  49437