1 EXIST(a):U(a)

Axiom

2 U(alf)

E Spec, 1

3 ALL(a):[U(a) => [F(a) => G(a)]]

& ALL(a):[U(a) => F(a)]

Premise

4 ALL(a):[U(a) => [F(a) => G(a)]]

Split, 3

5 ALL(a):[U(a) => F(a)]

Split, 3

6 U(alf) => F(alf)

U Spec, 5

7 F(alf)

Detach, 6, 2

8 U(alf) => [F(alf) => G(alf)]

U Spec, 4

9 F(alf) => G(alf)

Detach, 8, 2

10 G(alf)

Detach, 9, 7

11 ALL(a):[U(a) => [F(a) => G(a)]]

& ALL(a):[U(a) => F(a)]

=> G(alf)

4 Conclusion, 3

12 U(alf)

& [ALL(a):[U(a) => [F(a) => G(a)]]

& ALL(a):[U(a) => F(a)]

=> G(alf)]

Join, 2, 11

13 EXIST(alf):[U(alf)

& [ALL(a):[U(a) => [F(a) => G(a)]]

& ALL(a):[U(a) => F(a)]

=> G(alf)]]

E Gen, 12