Theorem ssrind 4166

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

Syntax hints:   → wi 4   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  fictb  9932  isacs1i  17283  rescabs  17464  lsmdisj  19202  dmdprdsplit2lem  19563  acsfn1p  19982  obselocv  20845  restbas  22217  neitr  22239  restcls  22240  restntr  22241  nrmsep  22416  cldllycmp  22554  fclsneii  23076  tsmsres  23203  trcfilu  23354  metdseq0  23923  iundisj2  24618  uniioombllem3  24654  ppisval  26158  ppisval2  26159  chtwordi  26210  ppiwordi  26216  chpub  26273  chebbnd1lem1  26522  mdbr2  30559  mdslj1i  30582  mdsl2i  30585  mdslmd1lem1  30588  mdslmd3i  30595  mdexchi  30598  sumdmdlem  30681  iundisj2f  30830  iundisj2fi  31020  cycpmco2f1  31293  tocyccntz  31313  esumrnmpt2  31936  bnj1177  32886  sstotbnd2  35859  lcvexchlem5  36979  pnonsingN  37874  dochnoncon  39332  eldioph2lem2  40499  limsupres  43136  limsupresxr  43197  liminfresxr  43198  liminflelimsuplem  43206  rhmsscrnghm  45472  rngcresringcat  45476  ssdisjd  46041