Theorem ssrind 4207

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  fictb  10197  isacs1i  17618  rescabs  17795  lsmdisj  19611  dmdprdsplit2lem  19977  rhmsscrnghm  20574  rngcresringcat  20578  acsfn1p  20708  obselocv  21637  restbas  23045  neitr  23067  restcls  23068  restntr  23069  nrmsep  23244  cldllycmp  23382  fclsneii  23904  tsmsres  24031  trcfilu  24181  metdseq0  24743  iundisj2  25450  uniioombllem3  25486  ppisval  27014  ppisval2  27015  chtwordi  27066  ppiwordi  27072  chpub  27131  chebbnd1lem1  27380  mdbr2  32225  mdslj1i  32248  mdsl2i  32251  mdslmd1lem1  32254  mdslmd3i  32261  mdexchi  32264  sumdmdlem  32347  iundisj2f  32519  iundisj2fi  32720  cycpmco2f1  33081  tocyccntz  33101  esumrnmpt2  34058  bnj1177  34996  sstotbnd2  37768  lcvexchlem5  39031  pnonsingN  39927  dochnoncon  41385  eldioph2lem2  42749  limsupres  45703  limsupresxr  45764  liminfresxr  45765  liminflelimsuplem  45773  ssdisjd  48796