# 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 ${⊢}\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 }$