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 17	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-in 3912  df-ss 3922

This theorem is referenced by:  fictb  10157  isacs1i  17581  rescabs  17758  lsmdisj  19578  dmdprdsplit2lem  19944  rhmsscrnghm  20568  rngcresringcat  20572  acsfn1p  20702  obselocv  21653  restbas  23061  neitr  23083  restcls  23084  restntr  23085  nrmsep  23260  cldllycmp  23398  fclsneii  23920  tsmsres  24047  trcfilu  24197  metdseq0  24759  iundisj2  25466  uniioombllem3  25502  ppisval  27030  ppisval2  27031  chtwordi  27082  ppiwordi  27088  chpub  27147  chebbnd1lem1  27396  mdbr2  32258  mdslj1i  32281  mdsl2i  32284  mdslmd1lem1  32287  mdslmd3i  32294  mdexchi  32297  sumdmdlem  32380  iundisj2f  32552  iundisj2fi  32753  cycpmco2f1  33079  tocyccntz  33099  esumrnmpt2  34034  bnj1177  34972  sstotbnd2  37753  lcvexchlem5  39016  pnonsingN  39912  dochnoncon  41370  eldioph2lem2  42734  limsupres  45687  limsupresxr  45748  liminfresxr  45749  liminflelimsuplem  45757  ssdisjd  48793