Theorem ssrind 4192

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

This proof depends on syntax axioms:   → wi 4   ∩ cin 3901   ⊆ wss 3902

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  fictb  10250  isacs1i  17751  rescabs  17928  lsmdisj  19814  dmdprdsplit2lem  20180  rhmsscrnghm  20833  rngcresringcat  20837  acsfn1p  20971  obselocv  21947  restbas  23389  neitr  23411  restcls  23412  restntr  23413  nrmsep  23588  cldllycmp  23727  fclsneii  24249  tsmsres  24376  trcfilu  24525  metdseq0  25087  iundisj2  25783  uniioombllem3  25819  ppisval  27348  ppisval2  27349  chtwordi  27400  ppiwordi  27406  chpub  27464  chebbnd1lem1  27713  mdbr2  32785  mdslj1i  32808  mdsl2i  32811  mdslmd1lem1  32814  mdslmd3i  32821  mdexchi  32824  sumdmdlem  32907  iundisj2f  33071  iundisj2fi  33276  cycpmco2f1  33572  tocyccntz  33592  esumrnmpt2  34586  bnj1177  35523  sstotbnd2  38532  lcvexchlem5  39919  pnonsingN  40814  dochnoncon  42272  eldioph2lem2  43614  limsupres  46541  limsupresxr  46602  liminfresxr  46603  liminflelimsuplem  46611  ssdisjd  49744