Mathematica Mathematical Logic: For all and There exists

[Goldenwind]

Mathematical Logic: "For all" and "There exists"

I need to show that
\vdash (\forall x)(A \rightarrow (B \equiv C)) \rightarrow ((\forall x)(A \rightarrow B) \equiv (\forall x)(A \rightarrow C))

My question to you, how does the (\forall x) affect this equation? If they weren't there, I could simply do this question, but their presence is confusing me. What's different? Can I just ignore them and move on as normal?

 

[varygoode]

Are your "\rightarrow" symbols for "implies"? If so, use \Rightarrow next time, so it isn't so confusing.

Now, with the notation you chose, I don't really understand what the entire statement is conjecturing. Please explain (in words) what you are trying to ask. (Besides the question about \forall x.)

 

[Goldenwind]

I wrote the symbols exactly how I was taught, sorry =/
I was taught that \rightarrow is used for "implies", or (¬A v B).

Now for what I'm trying to show... See the 2nd "implies" symbol? I'll be using the deduction theorem to move the (Ax)(A --> (B = C)) over to the left side of the |--, and then will attempt to work with the remaining right side of the |-- to show that it can be expressed the same as the left.

The thing is, my methods work when (Ax) isn't there, however I'm not sure if they work the same when it is. Can I just ignore the presence of (Ax), and do this question as if it weren't there?