Theorem ssrind 4244

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

Syntax hints:   → wi 4   ∩ cin 3950   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  fictb  10284  isacs1i  17700  rescabs  17877  rescabsOLD  17878  lsmdisj  19699  dmdprdsplit2lem  20065  rhmsscrnghm  20665  rngcresringcat  20669  acsfn1p  20800  obselocv  21748  restbas  23166  neitr  23188  restcls  23189  restntr  23190  nrmsep  23365  cldllycmp  23503  fclsneii  24025  tsmsres  24152  trcfilu  24303  metdseq0  24876  iundisj2  25584  uniioombllem3  25620  ppisval  27147  ppisval2  27148  chtwordi  27199  ppiwordi  27205  chpub  27264  chebbnd1lem1  27513  mdbr2  32315  mdslj1i  32338  mdsl2i  32341  mdslmd1lem1  32344  mdslmd3i  32351  mdexchi  32354  sumdmdlem  32437  iundisj2f  32603  iundisj2fi  32799  cycpmco2f1  33144  tocyccntz  33164  esumrnmpt2  34069  bnj1177  35020  sstotbnd2  37781  lcvexchlem5  39039  pnonsingN  39935  dochnoncon  41393  eldioph2lem2  42772  limsupres  45720  limsupresxr  45781  liminfresxr  45782  liminflelimsuplem  45790  ssdisjd  48727