Theorem ssrind 4195

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

Syntax hints:   → wi 4   ∩ cin 3903   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-ss 3921

This theorem is referenced by:  fictb  10197  isacs1i  17672  rescabs  17849  lsmdisj  19704  dmdprdsplit2lem  20070  rhmsscrnghm  20694  rngcresringcat  20698  acsfn1p  20828  obselocv  21760  restbas  23198  neitr  23220  restcls  23221  restntr  23222  nrmsep  23397  cldllycmp  23535  fclsneii  24057  tsmsres  24184  trcfilu  24333  metdseq0  24895  iundisj2  25591  uniioombllem3  25627  ppisval  27145  ppisval2  27146  chtwordi  27197  ppiwordi  27203  chpub  27261  chebbnd1lem1  27510  mdbr2  32445  mdslj1i  32468  mdsl2i  32471  mdslmd1lem1  32474  mdslmd3i  32481  mdexchi  32484  sumdmdlem  32567  iundisj2f  32739  iundisj2fi  32949  cycpmco2f1  33265  tocyccntz  33285  esumrnmpt2  34326  bnj1177  35265  sstotbnd2  38237  lcvexchlem5  39626  pnonsingN  40521  dochnoncon  41979  eldioph2lem2  43306  limsupres  46243  limsupresxr  46304  liminfresxr  46305  liminflelimsuplem  46313  ssdisjd  49393