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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-ss 3924

This theorem is referenced by:  fictb  10215  isacs1i  17701  rescabs  17878  lsmdisj  19739  dmdprdsplit2lem  20105  rhmsscrnghm  20738  rngcresringcat  20742  acsfn1p  20868  obselocv  21835  restbas  23272  neitr  23294  restcls  23295  restntr  23296  nrmsep  23471  cldllycmp  23609  fclsneii  24131  tsmsres  24258  trcfilu  24407  metdseq0  24969  iundisj2  25665  uniioombllem3  25701  ppisval  27222  ppisval2  27223  chtwordi  27274  ppiwordi  27280  chpub  27338  chebbnd1lem1  27587  mdbr2  32553  mdslj1i  32576  mdsl2i  32579  mdslmd1lem1  32582  mdslmd3i  32589  mdexchi  32592  sumdmdlem  32675  iundisj2f  32841  iundisj2fi  33050  cycpmco2f1  33352  tocyccntz  33372  esumrnmpt2  34370  bnj1177  35306  sstotbnd2  38280  lcvexchlem5  39669  pnonsingN  40564  dochnoncon  42022  eldioph2lem2  43349  limsupres  46278  limsupresxr  46339  liminfresxr  46340  liminflelimsuplem  46348  ssdisjd  49438