Theorem pm2.61danel

Description: Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021)

	Ref	Expression
Hypotheses	pm2.61danel.1	$$⊢\left(\phi \wedge A\in B\right)\to \psi$$
	pm2.61danel.2	$$⊢\left(\phi \wedge A\notin B\right)\to \psi$$
Assertion	pm2.61danel	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.61danel.1	$$⊢\left(\phi \wedge A\in B\right)\to \psi$$
2		pm2.61danel.2	$$⊢\left(\phi \wedge A\notin B\right)\to \psi$$
3		df-nel	$$⊢A\notin B\leftrightarrow \neg A\in B$$
4	3 2	sylan2br	$$⊢\left(\phi \wedge \neg A\in B\right)\to \psi$$
5	1 4	pm2.61dan	$$⊢\phi \to \psi$$