Theorem ssrind 4184

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

Syntax hints:   → wi 4   ∩ cin 3888   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  fictb  10166  isacs1i  17623  rescabs  17800  lsmdisj  19656  dmdprdsplit2lem  20022  rhmsscrnghm  20642  rngcresringcat  20646  acsfn1p  20776  obselocv  21708  restbas  23123  neitr  23145  restcls  23146  restntr  23147  nrmsep  23322  cldllycmp  23460  fclsneii  23982  tsmsres  24109  trcfilu  24258  metdseq0  24820  iundisj2  25516  uniioombllem3  25552  ppisval  27067  ppisval2  27068  chtwordi  27119  ppiwordi  27125  chpub  27183  chebbnd1lem1  27432  mdbr2  32367  mdslj1i  32390  mdsl2i  32393  mdslmd1lem1  32396  mdslmd3i  32403  mdexchi  32406  sumdmdlem  32489  iundisj2f  32660  iundisj2fi  32870  cycpmco2f1  33185  tocyccntz  33205  esumrnmpt2  34212  bnj1177  35148  sstotbnd2  38095  lcvexchlem5  39484  pnonsingN  40379  dochnoncon  41837  eldioph2lem2  43193  limsupres  46133  limsupresxr  46194  liminfresxr  46195  liminflelimsuplem  46203  ssdisjd  49283