Theorem ssrind 4193

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

Syntax hints:   → wi 4   ∩ cin 3897   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-ss 3915

This theorem is referenced by:  fictb  10142  isacs1i  17565  rescabs  17742  lsmdisj  19595  dmdprdsplit2lem  19961  rhmsscrnghm  20582  rngcresringcat  20586  acsfn1p  20716  obselocv  21667  restbas  23074  neitr  23096  restcls  23097  restntr  23098  nrmsep  23273  cldllycmp  23411  fclsneii  23933  tsmsres  24060  trcfilu  24209  metdseq0  24771  iundisj2  25478  uniioombllem3  25514  ppisval  27042  ppisval2  27043  chtwordi  27094  ppiwordi  27100  chpub  27159  chebbnd1lem1  27408  mdbr2  32278  mdslj1i  32301  mdsl2i  32304  mdslmd1lem1  32307  mdslmd3i  32314  mdexchi  32317  sumdmdlem  32400  iundisj2f  32572  iundisj2fi  32784  cycpmco2f1  33100  tocyccntz  33120  esumrnmpt2  34102  bnj1177  35039  sstotbnd2  37835  lcvexchlem5  39158  pnonsingN  40053  dochnoncon  41511  eldioph2lem2  42879  limsupres  45828  limsupresxr  45889  liminfresxr  45890  liminflelimsuplem  45898  ssdisjd  48933