Theorem pm2.61da2ne

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

	Ref	Expression
Hypotheses	pm2.61da2ne.1	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 )
	pm2.61da2ne.2	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝜓 )
	pm2.61da2ne.3	⊢ ( ( 𝜑 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ) ) → 𝜓 )
Assertion	pm2.61da2ne	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		pm2.61da2ne.1	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 )
2		pm2.61da2ne.2	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐷 ) → 𝜓 )
3		pm2.61da2ne.3	⊢ ( ( 𝜑 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ) ) → 𝜓 )
4	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 = 𝐷 ) → 𝜓 )
5	3	anassrs	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ≠ 𝐷 ) → 𝜓 )
6	4 5	pm2.61dane	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝜓 )
7	1 6	pm2.61dane	⊢ ( 𝜑 → 𝜓 )