Theorem ssrind 4173

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

Syntax hints:   → wi 4   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900

This theorem is referenced by:  fictb  10158  isacs1i  17615  rescabs  17792  lsmdisj  19648  dmdprdsplit2lem  20014  rhmsscrnghm  20638  rngcresringcat  20642  acsfn1p  20772  obselocv  21704  restbas  23142  neitr  23164  restcls  23165  restntr  23166  nrmsep  23341  cldllycmp  23479  fclsneii  24001  tsmsres  24128  trcfilu  24277  metdseq0  24839  iundisj2  25535  uniioombllem3  25571  ppisval  27086  ppisval2  27087  chtwordi  27138  ppiwordi  27144  chpub  27202  chebbnd1lem1  27451  mdbr2  32386  mdslj1i  32409  mdsl2i  32412  mdslmd1lem1  32415  mdslmd3i  32422  mdexchi  32425  sumdmdlem  32508  iundisj2f  32680  iundisj2fi  32890  cycpmco2f1  33206  tocyccntz  33226  esumrnmpt2  34261  bnj1177  35197  sstotbnd2  38150  lcvexchlem5  39539  pnonsingN  40434  dochnoncon  41892  eldioph2lem2  43219  limsupres  46156  limsupresxr  46217  liminfresxr  46218  liminflelimsuplem  46226  ssdisjd  49306