Theorem ssrind 4224

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

Syntax hints:   → wi 4   ∩ cin 3930   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-in 3938  df-ss 3948

This theorem is referenced by:  fictb  10266  isacs1i  17671  rescabs  17848  rescabsOLD  17849  lsmdisj  19667  dmdprdsplit2lem  20033  rhmsscrnghm  20633  rngcresringcat  20637  acsfn1p  20768  obselocv  21702  restbas  23112  neitr  23134  restcls  23135  restntr  23136  nrmsep  23311  cldllycmp  23449  fclsneii  23971  tsmsres  24098  trcfilu  24248  metdseq0  24812  iundisj2  25520  uniioombllem3  25556  ppisval  27083  ppisval2  27084  chtwordi  27135  ppiwordi  27141  chpub  27200  chebbnd1lem1  27449  mdbr2  32243  mdslj1i  32266  mdsl2i  32269  mdslmd1lem1  32272  mdslmd3i  32279  mdexchi  32282  sumdmdlem  32365  iundisj2f  32538  iundisj2fi  32738  cycpmco2f1  33083  tocyccntz  33103  esumrnmpt2  34028  bnj1177  34979  sstotbnd2  37740  lcvexchlem5  38998  pnonsingN  39894  dochnoncon  41352  eldioph2lem2  42735  limsupres  45677  limsupresxr  45738  liminfresxr  45739  liminflelimsuplem  45747  ssdisjd  48685