How would I represent a simple proof in Mathematica, such as x == 2 => x * x == 4?

Questions
1

I guess something like this would return true or false, depending on whether the implication holds true or not. Is there a way to do this?

2

If you try

Simplify[p,q]

Mathematica will try to simplify p given the information supplied in q.

For your example

Simplify[x*x==4,x==2]

returns

True

See if that will do the kinds of things you are looking for.

3

There are utilities for manipulating equations. Using them in sequence result in a proof:

x == 2
ApplySides[#^2 &, %]

This gives the result without proof:

Reduce[x == 2 \[Implies] x*x == 4]