Theorem ssrind 4227

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 4225	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∩ cin 3939   ⊆ wss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  fictb  10235  isacs1i  17597  rescabs  17778  rescabsOLD  17779  lsmdisj  19586  dmdprdsplit2lem  19952  rhmsscrnghm  20546  rngcresringcat  20550  acsfn1p  20635  obselocv  21583  restbas  22972  neitr  22994  restcls  22995  restntr  22996  nrmsep  23171  cldllycmp  23309  fclsneii  23831  tsmsres  23958  trcfilu  24109  metdseq0  24680  iundisj2  25388  uniioombllem3  25424  ppisval  26940  ppisval2  26941  chtwordi  26992  ppiwordi  26998  chpub  27057  chebbnd1lem1  27306  mdbr2  31973  mdslj1i  31996  mdsl2i  31999  mdslmd1lem1  32002  mdslmd3i  32009  mdexchi  32012  sumdmdlem  32095  iundisj2f  32245  iundisj2fi  32432  cycpmco2f1  32710  tocyccntz  32730  esumrnmpt2  33521  bnj1177  34472  sstotbnd2  37098  lcvexchlem5  38364  pnonsingN  39260  dochnoncon  40718  eldioph2lem2  41954  limsupres  44872  limsupresxr  44933  liminfresxr  44934  liminflelimsuplem  44942  ssdisjd  47646