Theorem ssrind 4219

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

Syntax hints:   → wi 4   ∩ cin 3925   ⊆ 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  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  fictb  10258  isacs1i  17669  rescabs  17846  lsmdisj  19662  dmdprdsplit2lem  20028  rhmsscrnghm  20625  rngcresringcat  20629  acsfn1p  20759  obselocv  21688  restbas  23096  neitr  23118  restcls  23119  restntr  23120  nrmsep  23295  cldllycmp  23433  fclsneii  23955  tsmsres  24082  trcfilu  24232  metdseq0  24794  iundisj2  25502  uniioombllem3  25538  ppisval  27066  ppisval2  27067  chtwordi  27118  ppiwordi  27124  chpub  27183  chebbnd1lem1  27432  mdbr2  32277  mdslj1i  32300  mdsl2i  32303  mdslmd1lem1  32306  mdslmd3i  32313  mdexchi  32316  sumdmdlem  32399  iundisj2f  32571  iundisj2fi  32774  cycpmco2f1  33135  tocyccntz  33155  esumrnmpt2  34099  bnj1177  35037  sstotbnd2  37798  lcvexchlem5  39056  pnonsingN  39952  dochnoncon  41410  eldioph2lem2  42784  limsupres  45734  limsupresxr  45795  liminfresxr  45796  liminflelimsuplem  45804  ssdisjd  48786