Theorem imadisjld

Description: Natural dduction form of one side of imadisj . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypothesis	imadisjld.1	$$⊢\phi \to \mathrm{dom}A\cap B=\varnothing$$
Assertion	imadisjld	$$⊢\phi \to A\left[B\right]=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		imadisjld.1	$$⊢\phi \to \mathrm{dom}A\cap B=\varnothing$$
2		imadisj	$$⊢A\left[B\right]=\varnothing \leftrightarrow \mathrm{dom}A\cap B=\varnothing$$
3	1 2	sylibr	$$⊢\phi \to A\left[B\right]=\varnothing$$