1 EY:AX:p(X,Y) Premise 2 AX:p(X,d) Assumption 3 p(c,d) Universal Elimination 2 4 EY:p(c,Y) Existential Introduction 3 5 AX:p(X,d) => EY:p(c,Y) Implication Introduction 2 4 6 AY:(AX:p(X,Y) => EY:p(c,Y)) Universal Introduction 5 7 EY:p(c,Y) Existential Elimination 1 6 8 AX:EY:p(X,Y) Universal Introduction 7 1 AX:(p(X) => q(X)) Premise 2 AX:p(X) Assumption 3 p(c) Universal Elimination 2 4 p(c) => q(c) Universal Elimination 1 5 q(c) Implication Elimination 4 3 6 AX:q(X) Universal Introduction 5 7 AX:p(X) => AX:q(X) Implication Introduction 2 6 1 AX:AY:p(X,Y) Premise 2 AY:p(c,Y) Universal Elimination 1 3 p(c,d) Universal Elimination 2 4 AX:p(X,d) Universal Introduction 3 5 AY:AX:p(X,Y) Universal Introduction 4