Theorem ssrind 4142

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

Syntax hints:   → wi 4   ∩ cin 3859   ⊆ wss 3860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877

This theorem is referenced by:  fictb  9718  isacs1i  17000  rescabs  17176  lsmdisj  18888  dmdprdsplit2lem  19249  acsfn1p  19660  obselocv  20507  restbas  21872  neitr  21894  restcls  21895  restntr  21896  nrmsep  22071  cldllycmp  22209  fclsneii  22731  tsmsres  22858  trcfilu  23009  metdseq0  23569  iundisj2  24263  uniioombllem3  24299  ppisval  25802  ppisval2  25803  chtwordi  25854  ppiwordi  25860  chpub  25917  chebbnd1lem1  26166  mdbr2  30192  mdslj1i  30215  mdsl2i  30218  mdslmd1lem1  30221  mdslmd3i  30228  mdexchi  30231  sumdmdlem  30314  iundisj2f  30465  iundisj2fi  30655  cycpmco2f1  30930  tocyccntz  30950  esumrnmpt2  31568  bnj1177  32519  sstotbnd2  35527  lcvexchlem5  36649  pnonsingN  37544  dochnoncon  39002  eldioph2lem2  40120  limsupres  42758  limsupresxr  42819  liminfresxr  42820  liminflelimsuplem  42828  rhmsscrnghm  45076  rngcresringcat  45080  ssdisjd  45637