Theorem disjimin

Description: Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021) (Revised by Peter Mazsa, 28-Sep-2021)

	Ref	Expression
Assertion	disjimin	$$⊢DisjS\to Disj\left(R\cap S\right)$$

Proof

Step	Hyp	Ref	Expression
1		inss2	$$⊢R\cap S\subseteq S$$
2	1	disjssi	$$⊢DisjS\to Disj\left(R\cap S\right)$$