Theorem ssrind 4194

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

Syntax hints:   → wi 4   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3909  df-ss 3919

This theorem is referenced by:  fictb  10135  isacs1i  17563  rescabs  17740  lsmdisj  19594  dmdprdsplit2lem  19960  rhmsscrnghm  20581  rngcresringcat  20585  acsfn1p  20715  obselocv  21666  restbas  23074  neitr  23096  restcls  23097  restntr  23098  nrmsep  23273  cldllycmp  23411  fclsneii  23933  tsmsres  24060  trcfilu  24209  metdseq0  24771  iundisj2  25478  uniioombllem3  25514  ppisval  27042  ppisval2  27043  chtwordi  27094  ppiwordi  27100  chpub  27159  chebbnd1lem1  27408  mdbr2  32274  mdslj1i  32297  mdsl2i  32300  mdslmd1lem1  32303  mdslmd3i  32310  mdexchi  32313  sumdmdlem  32396  iundisj2f  32568  iundisj2fi  32777  cycpmco2f1  33091  tocyccntz  33111  esumrnmpt2  34079  bnj1177  35016  sstotbnd2  37820  lcvexchlem5  39083  pnonsingN  39978  dochnoncon  41436  eldioph2lem2  42800  limsupres  45749  limsupresxr  45810  liminfresxr  45811  liminflelimsuplem  45819  ssdisjd  48845