Theorem ssrind 4162

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

Syntax hints:   → wi 4   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  fictb  9656  isacs1i  16920  rescabs  17095  lsmdisj  18799  dmdprdsplit2lem  19160  acsfn1p  19571  obselocv  20417  restbas  21763  neitr  21785  restcls  21786  restntr  21787  nrmsep  21962  cldllycmp  22100  fclsneii  22622  tsmsres  22749  trcfilu  22900  metdseq0  23459  iundisj2  24153  uniioombllem3  24189  ppisval  25689  ppisval2  25690  chtwordi  25741  ppiwordi  25747  chpub  25804  chebbnd1lem1  26053  mdbr2  30079  mdslj1i  30102  mdsl2i  30105  mdslmd1lem1  30108  mdslmd3i  30115  mdexchi  30118  sumdmdlem  30201  iundisj2f  30353  iundisj2fi  30546  cycpmco2f1  30816  tocyccntz  30836  esumrnmpt2  31437  bnj1177  32388  sstotbnd2  35212  lcvexchlem5  36334  pnonsingN  37229  dochnoncon  38687  eldioph2lem2  39702  limsupres  42347  limsupresxr  42408  liminfresxr  42409  liminflelimsuplem  42417  rhmsscrnghm  44650  rngcresringcat  44654