Theorem ssrind 4210

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

Syntax hints:   → wi 4   ∩ cin 3916   ⊆ wss 3917

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  fictb  10204  isacs1i  17625  rescabs  17802  lsmdisj  19618  dmdprdsplit2lem  19984  rhmsscrnghm  20581  rngcresringcat  20585  acsfn1p  20715  obselocv  21644  restbas  23052  neitr  23074  restcls  23075  restntr  23076  nrmsep  23251  cldllycmp  23389  fclsneii  23911  tsmsres  24038  trcfilu  24188  metdseq0  24750  iundisj2  25457  uniioombllem3  25493  ppisval  27021  ppisval2  27022  chtwordi  27073  ppiwordi  27079  chpub  27138  chebbnd1lem1  27387  mdbr2  32232  mdslj1i  32255  mdsl2i  32258  mdslmd1lem1  32261  mdslmd3i  32268  mdexchi  32271  sumdmdlem  32354  iundisj2f  32526  iundisj2fi  32727  cycpmco2f1  33088  tocyccntz  33108  esumrnmpt2  34065  bnj1177  35003  sstotbnd2  37775  lcvexchlem5  39038  pnonsingN  39934  dochnoncon  41392  eldioph2lem2  42756  limsupres  45710  limsupresxr  45771  liminfresxr  45772  liminflelimsuplem  45780  ssdisjd  48800