Theorem ssrind 4235

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

Syntax hints:   → wi 4   ∩ cin 3947   ⊆ wss 3948

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  fictb  10246  isacs1i  17608  rescabs  17789  rescabsOLD  17790  lsmdisj  19597  dmdprdsplit2lem  19963  rhmsscrnghm  20557  rngcresringcat  20561  acsfn1p  20646  obselocv  21593  restbas  22982  neitr  23004  restcls  23005  restntr  23006  nrmsep  23181  cldllycmp  23319  fclsneii  23841  tsmsres  23968  trcfilu  24119  metdseq0  24690  iundisj2  25398  uniioombllem3  25434  ppisval  26949  ppisval2  26950  chtwordi  27001  ppiwordi  27007  chpub  27066  chebbnd1lem1  27315  mdbr2  31982  mdslj1i  32005  mdsl2i  32008  mdslmd1lem1  32011  mdslmd3i  32018  mdexchi  32021  sumdmdlem  32104  iundisj2f  32254  iundisj2fi  32441  cycpmco2f1  32719  tocyccntz  32739  esumrnmpt2  33530  bnj1177  34481  sstotbnd2  37106  lcvexchlem5  38372  pnonsingN  39268  dochnoncon  40726  eldioph2lem2  41962  limsupres  44880  limsupresxr  44941  liminfresxr  44942  liminflelimsuplem  44950  ssdisjd  47654