Theorem ssrind 4143

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  fictb  10352  isacs1i  17863  rescabs  18040  lsmdisj  19928  dmdprdsplit2lem  20294  rhmsscrnghm  20950  rngcresringcat  20954  acsfn1p  21089  obselocv  22067  restbas  23509  neitr  23531  restcls  23532  restntr  23533  nrmsep  23708  cldllycmp  23847  fclsneii  24369  tsmsres  24496  trcfilu  24645  metdseq0  25207  iundisj2  25903  uniioombllem3  25939  ppisval  27464  ppisval2  27465  chtwordi  27516  ppiwordi  27522  chpub  27580  chebbnd1lem1  27829  mdbr2  32931  mdslj1i  32954  mdsl2i  32957  mdslmd1lem1  32960  mdslmd3i  32967  mdexchi  32970  sumdmdlem  33053  iundisj2f  33259  iundisj2fi  33462  cycpmco2f1  33761  tocyccntz  33781  esumrnmpt2  34783  bnj1177  35719  sstotbnd2  38911  lcvexchlem5  40298  pnonsingN  41193  dochnoncon  42651  eldioph2lem2  43976  limsupres  46930  limsupresxr  46991  liminfresxr  46992  liminflelimsuplem  47000  ssdisjd  50133