Theorem ssrind 4169

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

Syntax hints:   → wi 4   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  fictb  10001  isacs1i  17366  rescabs  17547  rescabsOLD  17548  lsmdisj  19287  dmdprdsplit2lem  19648  acsfn1p  20067  obselocv  20935  restbas  22309  neitr  22331  restcls  22332  restntr  22333  nrmsep  22508  cldllycmp  22646  fclsneii  23168  tsmsres  23295  trcfilu  23446  metdseq0  24017  iundisj2  24713  uniioombllem3  24749  ppisval  26253  ppisval2  26254  chtwordi  26305  ppiwordi  26311  chpub  26368  chebbnd1lem1  26617  mdbr2  30658  mdslj1i  30681  mdsl2i  30684  mdslmd1lem1  30687  mdslmd3i  30694  mdexchi  30697  sumdmdlem  30780  iundisj2f  30929  iundisj2fi  31118  cycpmco2f1  31391  tocyccntz  31411  esumrnmpt2  32036  bnj1177  32986  sstotbnd2  35932  lcvexchlem5  37052  pnonsingN  37947  dochnoncon  39405  eldioph2lem2  40583  limsupres  43246  limsupresxr  43307  liminfresxr  43308  liminflelimsuplem  43316  rhmsscrnghm  45584  rngcresringcat  45588  ssdisjd  46153