Theorem ssrind 4036

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

Syntax hints:   → wi 4   ∩ cin 3769   ⊆ wss 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-v 3388  df-in 3777  df-ss 3784

This theorem is referenced by:  fictb  9356  isacs1i  16631  rescabs  16806  lsmdisj  18406  dmdprdsplit2lem  18759  obselocv  20396  restbas  21290  neitr  21312  restcls  21313  restntr  21314  nrmsep  21489  cldllycmp  21626  fclsneii  22148  tsmsres  22274  trcfilu  22425  metdseq0  22984  iundisj2  23656  uniioombllem3  23692  ppisval  25181  ppisval2  25182  chtwordi  25233  ppiwordi  25239  chpub  25296  chebbnd1lem1  25509  mdbr2  29679  mdslj1i  29702  mdsl2i  29705  mdslmd1lem1  29708  mdslmd3i  29715  mdexchi  29718  sumdmdlem  29801  iundisj2f  29919  iundisj2fi  30073  esumrnmpt2  30645  bnj1177  31590  sstotbnd2  34059  lcvexchlem5  35058  pnonsingN  35953  dochnoncon  37411  eldioph2lem2  38105  acsfn1p  38549  limsupres  40676  limsupresxr  40737  liminfresxr  40738  liminflelimsuplem  40746  rhmsscrnghm  42820  rngcresringcat  42824