Theorem ssrind 4198

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  fictb  10166  isacs1i  17592  rescabs  17769  lsmdisj  19622  dmdprdsplit2lem  19988  rhmsscrnghm  20610  rngcresringcat  20614  acsfn1p  20744  obselocv  21695  restbas  23114  neitr  23136  restcls  23137  restntr  23138  nrmsep  23313  cldllycmp  23451  fclsneii  23973  tsmsres  24100  trcfilu  24249  metdseq0  24811  iundisj2  25518  uniioombllem3  25554  ppisval  27082  ppisval2  27083  chtwordi  27134  ppiwordi  27140  chpub  27199  chebbnd1lem1  27448  mdbr2  32383  mdslj1i  32406  mdsl2i  32409  mdslmd1lem1  32412  mdslmd3i  32419  mdexchi  32422  sumdmdlem  32505  iundisj2f  32676  iundisj2fi  32887  cycpmco2f1  33217  tocyccntz  33237  esumrnmpt2  34245  bnj1177  35181  sstotbnd2  38019  lcvexchlem5  39408  pnonsingN  40303  dochnoncon  41761  eldioph2lem2  43112  limsupres  46057  limsupresxr  46118  liminfresxr  46119  liminflelimsuplem  46127  ssdisjd  49161