Theorem ssrind 4200

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

Syntax hints:   → wi 4   ∩ cin 3912   ⊆ wss 3913

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  fictb  10190  isacs1i  17551  rescabs  17732  rescabsOLD  17733  lsmdisj  19477  dmdprdsplit2lem  19838  acsfn1p  20322  obselocv  21171  restbas  22546  neitr  22568  restcls  22569  restntr  22570  nrmsep  22745  cldllycmp  22883  fclsneii  23405  tsmsres  23532  trcfilu  23683  metdseq0  24254  iundisj2  24950  uniioombllem3  24986  ppisval  26490  ppisval2  26491  chtwordi  26542  ppiwordi  26548  chpub  26605  chebbnd1lem1  26854  mdbr2  31301  mdslj1i  31324  mdsl2i  31327  mdslmd1lem1  31330  mdslmd3i  31337  mdexchi  31340  sumdmdlem  31423  iundisj2f  31575  iundisj2fi  31768  cycpmco2f1  32043  tocyccntz  32063  esumrnmpt2  32756  bnj1177  33707  sstotbnd2  36306  lcvexchlem5  37573  pnonsingN  38469  dochnoncon  39927  eldioph2lem2  41142  limsupres  44066  limsupresxr  44127  liminfresxr  44128  liminflelimsuplem  44136  rhmsscrnghm  46444  rngcresringcat  46448  ssdisjd  47012