Theorem pm2.61dane

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011)

	Ref	Expression
Hypotheses	pm2.61dane.1	$$⊢\left(\phi \wedge A=B\right)\to \psi$$
	pm2.61dane.2	$$⊢\left(\phi \wedge A\ne B\right)\to \psi$$
Assertion	pm2.61dane	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.61dane.1	$$⊢\left(\phi \wedge A=B\right)\to \psi$$
2		pm2.61dane.2	$$⊢\left(\phi \wedge A\ne B\right)\to \psi$$
3	1	ex	$$⊢\phi \to \left(A=B\to \psi \right)$$
4	2	ex	$$⊢\phi \to \left(A\ne B\to \psi \right)$$
5	3 4	pm2.61dne	$$⊢\phi \to \psi$$