Theorem ssrind 4197

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3913  df-ss 3923

This theorem is referenced by:  fictb  10228  isacs1i  17714  rescabs  17891  lsmdisj  19752  dmdprdsplit2lem  20118  rhmsscrnghm  20751  rngcresringcat  20755  acsfn1p  20883  obselocv  21859  restbas  23296  neitr  23318  restcls  23319  restntr  23320  nrmsep  23495  cldllycmp  23633  fclsneii  24155  tsmsres  24282  trcfilu  24431  metdseq0  24993  iundisj2  25689  uniioombllem3  25725  ppisval  27249  ppisval2  27250  chtwordi  27301  ppiwordi  27307  chpub  27365  chebbnd1lem1  27614  mdbr2  32629  mdslj1i  32652  mdsl2i  32655  mdslmd1lem1  32658  mdslmd3i  32665  mdexchi  32668  sumdmdlem  32751  iundisj2f  32916  iundisj2fi  33123  cycpmco2f1  33425  tocyccntz  33445  esumrnmpt2  34439  bnj1177  35375  sstotbnd2  38406  lcvexchlem5  39793  pnonsingN  40688  dochnoncon  42146  eldioph2lem2  43475  limsupres  46402  limsupresxr  46463  liminfresxr  46464  liminflelimsuplem  46472  ssdisjd  49569