Theorem ssrind 4211

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

Syntax hints:   → wi 4   ∩ cin 3934   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951

This theorem is referenced by:  fictb  9661  isacs1i  16922  rescabs  17097  lsmdisj  18801  dmdprdsplit2lem  19161  acsfn1p  19572  obselocv  20866  restbas  21760  neitr  21782  restcls  21783  restntr  21784  nrmsep  21959  cldllycmp  22097  fclsneii  22619  tsmsres  22746  trcfilu  22897  metdseq0  23456  iundisj2  24144  uniioombllem3  24180  ppisval  25675  ppisval2  25676  chtwordi  25727  ppiwordi  25733  chpub  25790  chebbnd1lem1  26039  mdbr2  30067  mdslj1i  30090  mdsl2i  30093  mdslmd1lem1  30096  mdslmd3i  30103  mdexchi  30106  sumdmdlem  30189  iundisj2f  30334  iundisj2fi  30514  cycpmco2f1  30761  tocyccntz  30781  esumrnmpt2  31322  bnj1177  32273  sstotbnd2  35046  lcvexchlem5  36168  pnonsingN  37063  dochnoncon  38521  eldioph2lem2  39351  limsupres  41979  limsupresxr  42040  liminfresxr  42041  liminflelimsuplem  42049  rhmsscrnghm  44291  rngcresringcat  44295