Theorem ssrind 4196

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

Syntax hints:   → wi 4   ∩ cin 3900   ⊆ wss 3901

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  fictb  10154  isacs1i  17580  rescabs  17757  lsmdisj  19610  dmdprdsplit2lem  19976  rhmsscrnghm  20598  rngcresringcat  20602  acsfn1p  20732  obselocv  21683  restbas  23102  neitr  23124  restcls  23125  restntr  23126  nrmsep  23301  cldllycmp  23439  fclsneii  23961  tsmsres  24088  trcfilu  24237  metdseq0  24799  iundisj2  25506  uniioombllem3  25542  ppisval  27070  ppisval2  27071  chtwordi  27122  ppiwordi  27128  chpub  27187  chebbnd1lem1  27436  mdbr2  32371  mdslj1i  32394  mdsl2i  32397  mdslmd1lem1  32400  mdslmd3i  32407  mdexchi  32410  sumdmdlem  32493  iundisj2f  32665  iundisj2fi  32877  cycpmco2f1  33206  tocyccntz  33226  esumrnmpt2  34225  bnj1177  35162  sstotbnd2  37971  lcvexchlem5  39294  pnonsingN  40189  dochnoncon  41647  eldioph2lem2  42999  limsupres  45945  limsupresxr  46006  liminfresxr  46007  liminflelimsuplem  46015  ssdisjd  49049