Theorem ssrind 4251

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

Syntax hints:   → wi 4   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  fictb  10281  isacs1i  17701  rescabs  17882  rescabsOLD  17883  lsmdisj  19713  dmdprdsplit2lem  20079  rhmsscrnghm  20681  rngcresringcat  20685  acsfn1p  20816  obselocv  21765  restbas  23181  neitr  23203  restcls  23204  restntr  23205  nrmsep  23380  cldllycmp  23518  fclsneii  24040  tsmsres  24167  trcfilu  24318  metdseq0  24889  iundisj2  25597  uniioombllem3  25633  ppisval  27161  ppisval2  27162  chtwordi  27213  ppiwordi  27219  chpub  27278  chebbnd1lem1  27527  mdbr2  32324  mdslj1i  32347  mdsl2i  32350  mdslmd1lem1  32353  mdslmd3i  32360  mdexchi  32363  sumdmdlem  32446  iundisj2f  32609  iundisj2fi  32804  cycpmco2f1  33126  tocyccntz  33146  esumrnmpt2  34048  bnj1177  34998  sstotbnd2  37760  lcvexchlem5  39019  pnonsingN  39915  dochnoncon  41373  eldioph2lem2  42748  limsupres  45660  limsupresxr  45721  liminfresxr  45722  liminflelimsuplem  45730  ssdisjd  48655