# Metamath Proof Explorer

## Theorem pm2.61da3ne

Description: Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013) (Proof shortened by Wolf Lammen, 25-Nov-2019)

Ref Expression
Hypotheses pm2.61da3ne.1 ${⊢}\left({\phi }\wedge {A}={B}\right)\to {\psi }$
pm2.61da3ne.2 ${⊢}\left({\phi }\wedge {C}={D}\right)\to {\psi }$
pm2.61da3ne.3 ${⊢}\left({\phi }\wedge {E}={F}\right)\to {\psi }$
pm2.61da3ne.4 ${⊢}\left({\phi }\wedge \left({A}\ne {B}\wedge {C}\ne {D}\wedge {E}\ne {F}\right)\right)\to {\psi }$
Assertion pm2.61da3ne ${⊢}{\phi }\to {\psi }$

### Proof

Step Hyp Ref Expression
1 pm2.61da3ne.1 ${⊢}\left({\phi }\wedge {A}={B}\right)\to {\psi }$
2 pm2.61da3ne.2 ${⊢}\left({\phi }\wedge {C}={D}\right)\to {\psi }$
3 pm2.61da3ne.3 ${⊢}\left({\phi }\wedge {E}={F}\right)\to {\psi }$
4 pm2.61da3ne.4 ${⊢}\left({\phi }\wedge \left({A}\ne {B}\wedge {C}\ne {D}\wedge {E}\ne {F}\right)\right)\to {\psi }$
5 1 a1d ${⊢}\left({\phi }\wedge {A}={B}\right)\to \left(\left({C}\ne {D}\wedge {E}\ne {F}\right)\to {\psi }\right)$
6 4 3exp2 ${⊢}{\phi }\to \left({A}\ne {B}\to \left({C}\ne {D}\to \left({E}\ne {F}\to {\psi }\right)\right)\right)$
7 6 imp4b ${⊢}\left({\phi }\wedge {A}\ne {B}\right)\to \left(\left({C}\ne {D}\wedge {E}\ne {F}\right)\to {\psi }\right)$
8 5 7 pm2.61dane ${⊢}{\phi }\to \left(\left({C}\ne {D}\wedge {E}\ne {F}\right)\to {\psi }\right)$
9 8 imp ${⊢}\left({\phi }\wedge \left({C}\ne {D}\wedge {E}\ne {F}\right)\right)\to {\psi }$
10 2 3 9 pm2.61da2ne ${⊢}{\phi }\to {\psi }$