Can I use any variable to represent a much larger proposition?

Question

I have 3 premises

A. ∀x: S(x) → ¬∃y: K(y, x)
B. ∃x: ∃y: K(x, y)
C. ∃x: ¬S(x)

I'm trying to prove

(A ∧ B) → C

So I do the proof and eventually get the conclusion

((∀x: S(x) → ¬∃y: K(y, x)) ∧ (∃x: ∃y: K(x, y))) →  (∃x: ¬S(x))

Which I know is (A ∧ B) → C, but in a formal proof I can't just replace the individual propositions in the above statement with A, B, and C in order to get the conclusion I desire right?

So, I'm unsure of whether I have to start with the premises:

A ↔ ∀x: S(x) → ¬∃y: K(y, x)
B ↔ ∃x: ∃y: K(x, y)
C ↔ ∃x: ¬S(x)

In order to derive (A ∧ B) → C ? Or if I can just replace swap in the corresponding A, B, and C and get the conclusion.

Also, if I do have to start with a premise like: A ↔ ∀x: S(x) → ¬∃y: K(y, x) am I allowed to separate the ∀x: S(x) → ¬∃y: K(y, x) part that I need and work on it?

Answer 1

They are using the letters $A,B,C$ to represent entire propositions (including their respective quantifiers) and give you an idea of the form of the statement they want you to prove. You proved exactly what they asked you to prove. You may substitute the letters $A,B,C$ into your conclusion, if you wish, but it is not necessary. Again, I believe they were using the letters to give you an idea of what to prove. Nice work!

Answer 2

If $A$, $B$ and $C$ are premises, then one can derive $(A\land B)\to C$ as follows:

Notice that one only needs $C$ as a premise. So something else is going on here.

As RyRy the Fly Guy suggested they may want you to take as premises the first two statements and derive the third statement from those two. Here is how such a proof might look:

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/