Theorem ssdisjd

Description: Subset preserves disjointness. Deduction form of ssdisj . (Contributed by Zhi Wang, 7-Sep-2024)

	Ref	Expression
Hypotheses	ssdisjd.1	$$⊢\phi \to A\subseteq B$$
	ssdisjd.2	$$⊢\phi \to B\cap C=\varnothing$$
Assertion	ssdisjd	$$⊢\phi \to A\cap C=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ssdisjd.1	$$⊢\phi \to A\subseteq B$$
2		ssdisjd.2	$$⊢\phi \to B\cap C=\varnothing$$
3	1	ssrind	$$⊢\phi \to A\cap C\subseteq B\cap C$$
4		sseq0	$$⊢\left(A\cap C\subseteq B\cap C\wedge B\cap C=\varnothing \right)\to A\cap C=\varnothing$$
5	3 2 4	syl2anc	$$⊢\phi \to A\cap C=\varnothing$$