An earlier version of the question had five parts:
- ∀x(Px ∨ Q) ⊢ (∀xPx ∨ Q)
- ∀xPx → Q ⊢ ∃x(Px → Q)
- ∀x∀y(Rxy → ¬x = y) ⊢ ¬∃xRxx
- ∀x(∃yPxy → ∀yPyx) ⊢ ∃x∃yPxy → ∀x∀yPxy
- ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))
What remains in the question is only part 5.
Too many...
Hint for 1) :
1) ∀x(Px ∨ Q) --- premise
2) Px ∨ Q --- form 1) by ∀-elim
3) ¬Q --- assumed [a]
4) ∃x¬Px --- assumed [b]
5) Q --- assumed [c] from 2) for ∨-elim
6) ⊥ --- contradiction, from 3) and 5)
7) ¬¬Q --- from 3) and 6) by ¬-intro, discharging [a]
8) Q --- from 7) by ¬¬-elim
9) ∀xPx ∨ Q --- from 8) by ∨-intro
10) Px --- assumed [d] from 2) for ∨-elim
11) ¬Px --- assumed [e] from 4) for ∃-elim
12) ⊥ --- contradiction, from 10) and 11) and discharging [e] by ∃-elim
13) ¬∃x¬Px --- from 4) and 12) by ¬-intro, dicharging [b]
14) ∀Px --- from 13) using the sub-derivation ¬∃x¬ ⊢∀x : assume ¬Px, and then ∃x¬Px by ∃-intro. With contradiction, and double negation, derive Px, discharging the assumption, and conclude with ∀xPx by ∀-intro.
15) ∀Px ∨ Q --- from 14) by ∨-intro
16) ∀Px ∨ Q --- from 2) and 5)-9) and 10)-15) by ∨-elim, discharging [c] and [d].
Hint for 2) :
1) ∀xPx → Q --- premise
2) Px --- assumed [a]
3) ∃x¬Px --- assumed [b]
4) ¬Px --- assumed [c] from 3) for ∃-elim
5) ⊥ --- contradiction, from 2) and 4)
6) ⊥ --- from 3), 4) and 5) by ∃-elim, discharging [c]
7) ¬∃x¬Px --- from 3) and 6) by ¬¬-elim, dicharging [b]
8) ∀Px --- from 7) using the sub-derivation ¬∃x¬ ⊢∀x
9) Q --- from 1) and 8) by →-elim
10) Px → Q$ --- from 2) and 9) by →-intro, discharging [a]
11) ∃x(Px → Q) --- from 10) by ∃-intro.
Hint for 3) :
1) ∀x∀y(Rxy → ¬x = y) --- premise
2) Rxx --- assumed [a]
3) Rxx → ¬ x = x --- from 1 by ∀-elim
4) ¬ x = x --- from 2) and 3) by →-elim
5) x = x --- axiom for equality
6) ¬Rxx --- from 2) and contradiction, by ¬-intro, discharging [a]
7) ∀x¬Rxx --- from 6) by ∀-intro
Now we have to add the sub-derivation : ∀x¬ ⊢ ¬∃x.
The last one is long and tedious, but quite straightforward.
Hint for 5) :
1) ∃x∃y∀z(x = z ∨ y = z) --- premise
2) ¬∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- assume the negation of the conclusion and search for a contradiction: if found, the result will follow by ¬¬-elim
3) ∀z(a = z ∨ b = z) --- assumed from 1) for ∃-elim twice
4) ∃x∃y ¬(¬x = y → ∀z(x = z ∨ y = z)) --- from 2), playing again with the quantifiers equivalence
5) ¬(¬c = d → ∀z(c = z ∨ d = z)) --- assumed from 4) for ∃-elim twice
6) ¬c = d ∧ ¬∀z(c = z ∨ d = z) --- from 6) by tautological equivalence
7) ¬c = d --- from 6) by ∧-elim
8) ¬∀z(c = z ∨ d = z) --- from 6) by ∧-elim
9) ∃z ¬(c = z ∨ d = z) --- from 9) again by quantifiers equivalence
10) ¬(c = e ∨ d = e) --- assumed from 9) for ∃-elim
11) ¬c = e ∧ ¬d = e --- from 10) by tautological equivalence
12) ¬c = e --- from 11) by ∧-elim
13) ¬d = e --- from 11) by ∧-elim
Now we have to instantiate 3) ∀z(a = z ∨ b = z) trice, with c,d,e respectively, to get :
14) a = c ∨ b = c
15) a = d ∨ b = d
16) a = e ∨ b = e
and finelly get the desired contradiciton with 7), 12) and 13) (simple but boring application of ∨-elim).
What we get is :
20) ⊥
that closes all the ∃-elim's above, discharging the corresponding assumptions.
21) ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- from 2) and 20) by ¬¬-elim.