Theorem ssrind 4199

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

This proof depends on syntax axioms:   → wi 4   ∩ cin 3907   ⊆ wss 3908

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-in 3915  df-ss 3925

This theorem is used by:  fictb  10246  isacs1i  17738  rescabs  17915  lsmdisj  19782  dmdprdsplit2lem  20148  rhmsscrnghm  20801  rngcresringcat  20805  acsfn1p  20939  obselocv  21915  restbas  23352  neitr  23374  restcls  23375  restntr  23376  nrmsep  23551  cldllycmp  23689  fclsneii  24211  tsmsres  24338  trcfilu  24487  metdseq0  25049  iundisj2  25745  uniioombllem3  25781  ppisval  27305  ppisval2  27306  chtwordi  27357  ppiwordi  27363  chpub  27421  chebbnd1lem1  27670  mdbr2  32685  mdslj1i  32708  mdsl2i  32711  mdslmd1lem1  32714  mdslmd3i  32721  mdexchi  32724  sumdmdlem  32807  iundisj2f  32972  iundisj2fi  33179  cycpmco2f1  33475  tocyccntz  33495  esumrnmpt2  34489  bnj1177  35426  sstotbnd2  38466  lcvexchlem5  39853  pnonsingN  40748  dochnoncon  42206  eldioph2lem2  43533  limsupres  46460  limsupresxr  46521  liminfresxr  46522  liminflelimsuplem  46530  ssdisjd  49627