Theorem pm2.61da2ne

Description: Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.61da2ne.1	$$⊢\left(\phi \wedge A=B\right)\to \psi$$
2		pm2.61da2ne.2	$$⊢\left(\phi \wedge C=D\right)\to \psi$$
3		pm2.61da2ne.3	$$⊢\left(\phi \wedge \left(A\ne B\wedge C\ne D\right)\right)\to \psi$$
4	2	adantlr	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge C=D\right)\to \psi$$
5	3	anassrs	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge C\ne D\right)\to \psi$$
6	4 5	pm2.61dane	$$⊢\left(\phi \wedge A\ne B\right)\to \psi$$
7	1 6	pm2.61dane	$$⊢\phi \to \psi$$