Theorem ssrind 4179

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

Syntax hints:   → wi 4   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-in 3897  df-ss 3907

This theorem is referenced by:  fictb  10164  isacs1i  17621  rescabs  17798  lsmdisj  19654  dmdprdsplit2lem  20020  rhmsscrnghm  20644  rngcresringcat  20648  acsfn1p  20778  obselocv  21710  restbas  23148  neitr  23170  restcls  23171  restntr  23172  nrmsep  23347  cldllycmp  23485  fclsneii  24007  tsmsres  24134  trcfilu  24283  metdseq0  24845  iundisj2  25541  uniioombllem3  25577  ppisval  27092  ppisval2  27093  chtwordi  27144  ppiwordi  27150  chpub  27208  chebbnd1lem1  27457  mdbr2  32392  mdslj1i  32415  mdsl2i  32418  mdslmd1lem1  32421  mdslmd3i  32428  mdexchi  32431  sumdmdlem  32514  iundisj2f  32686  iundisj2fi  32896  cycpmco2f1  33212  tocyccntz  33232  esumrnmpt2  34259  bnj1177  35195  sstotbnd2  38148  lcvexchlem5  39537  pnonsingN  40432  dochnoncon  41890  eldioph2lem2  43217  limsupres  46155  limsupresxr  46216  liminfresxr  46217  liminflelimsuplem  46225  ssdisjd  49305