This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm2.61da2ne

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

Ref Expression
Hypotheses pm2.61da2ne.1 ⊢ φ ∧ A = B → ψ
pm2.61da2ne.2 ⊢ φ ∧ C = D → ψ
pm2.61da2ne.3 ⊢ φ ∧ A ≠ B ∧ C ≠ D → ψ
Assertion pm2.61da2ne ⊢ φ → ψ

Proof

Step Hyp Ref Expression
1 pm2.61da2ne.1 ⊢ φ ∧ A = B → ψ
2 pm2.61da2ne.2 ⊢ φ ∧ C = D → ψ
3 pm2.61da2ne.3 ⊢ φ ∧ A ≠ B ∧ C ≠ D → ψ
4 2 adantlr ⊢ φ ∧ A ≠ B ∧ C = D → ψ
5 3 anassrs ⊢ φ ∧ A ≠ B ∧ C ≠ D → ψ
6 4 5 pm2.61dane ⊢ φ ∧ A ≠ B → ψ
7 1 6 pm2.61dane ⊢ φ → ψ