Theorem ssrind 4189

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

This proof depends on syntax axioms:   → wi 4   ∩ cin 3898   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  fictb  10303  isacs1i  17811  rescabs  17988  lsmdisj  19875  dmdprdsplit2lem  20241  rhmsscrnghm  20897  rngcresringcat  20901  acsfn1p  21036  obselocv  22014  restbas  23456  neitr  23478  restcls  23479  restntr  23480  nrmsep  23655  cldllycmp  23794  fclsneii  24316  tsmsres  24443  trcfilu  24592  metdseq0  25154  iundisj2  25850  uniioombllem3  25886  ppisval  27413  ppisval2  27414  chtwordi  27465  ppiwordi  27471  chpub  27529  chebbnd1lem1  27778  mdbr2  32880  mdslj1i  32903  mdsl2i  32906  mdslmd1lem1  32909  mdslmd3i  32916  mdexchi  32919  sumdmdlem  33002  iundisj2f  33166  iundisj2fi  33371  cycpmco2f1  33667  tocyccntz  33687  esumrnmpt2  34682  bnj1177  35619  sstotbnd2  38676  lcvexchlem5  40063  pnonsingN  40958  dochnoncon  42416  eldioph2lem2  43725  limsupres  46659  limsupresxr  46720  liminfresxr  46721  liminflelimsuplem  46729  ssdisjd  49862