Theorem ssrind 4140

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  fictb  10326  isacs1i  17837  rescabs  18014  lsmdisj  19901  dmdprdsplit2lem  20267  rhmsscrnghm  20923  rngcresringcat  20927  acsfn1p  21062  obselocv  22040  restbas  23482  neitr  23504  restcls  23505  restntr  23506  nrmsep  23681  cldllycmp  23820  fclsneii  24342  tsmsres  24469  trcfilu  24618  metdseq0  25180  iundisj2  25876  uniioombllem3  25912  ppisval  27437  ppisval2  27438  chtwordi  27489  ppiwordi  27495  chpub  27553  chebbnd1lem1  27802  mdbr2  32904  mdslj1i  32927  mdsl2i  32930  mdslmd1lem1  32933  mdslmd3i  32940  mdexchi  32943  sumdmdlem  33026  iundisj2f  33232  iundisj2fi  33436  cycpmco2f1  33732  tocyccntz  33752  esumrnmpt2  34747  bnj1177  35683  sstotbnd2  38802  lcvexchlem5  40189  pnonsingN  41084  dochnoncon  42542  eldioph2lem2  43866  limsupres  46809  limsupresxr  46870  liminfresxr  46871  liminflelimsuplem  46879  ssdisjd  50012