Theorem ssrind 4265

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

Syntax hints:   → wi 4   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  fictb  10313  isacs1i  17715  rescabs  17896  rescabsOLD  17897  lsmdisj  19723  dmdprdsplit2lem  20089  rhmsscrnghm  20687  rngcresringcat  20691  acsfn1p  20822  obselocv  21771  restbas  23187  neitr  23209  restcls  23210  restntr  23211  nrmsep  23386  cldllycmp  23524  fclsneii  24046  tsmsres  24173  trcfilu  24324  metdseq0  24895  iundisj2  25603  uniioombllem3  25639  ppisval  27165  ppisval2  27166  chtwordi  27217  ppiwordi  27223  chpub  27282  chebbnd1lem1  27531  mdbr2  32328  mdslj1i  32351  mdsl2i  32354  mdslmd1lem1  32357  mdslmd3i  32364  mdexchi  32367  sumdmdlem  32450  iundisj2f  32612  iundisj2fi  32802  cycpmco2f1  33117  tocyccntz  33137  esumrnmpt2  34032  bnj1177  34982  sstotbnd2  37734  lcvexchlem5  38994  pnonsingN  39890  dochnoncon  41348  eldioph2lem2  42717  limsupres  45626  limsupresxr  45687  liminfresxr  45688  liminflelimsuplem  45696  ssdisjd  48539