Theorem pm2.21ddne

Description: A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	pm2.21ddne.1	$$⊢\phi \to A=B$$
	pm2.21ddne.2	$$⊢\phi \to A\ne B$$
Assertion	pm2.21ddne	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.21ddne.1	$$⊢\phi \to A=B$$
2		pm2.21ddne.2	$$⊢\phi \to A\ne B$$
3	2	neneqd	$$⊢\phi \to \neg A=B$$
4	1 3	pm2.21dd	$$⊢\phi \to \psi$$