Prooftoys in its current form can be used in two rather different but related ways. It can be used to explore and create simple proofs in mathematical logic. Or it can be used as a tool to help in solving basic algebra problems.
For practice with algebra problem solving, try the Mathtoys website. That site is powered by the same Prooftoys software that powers this one, but the Mathtoys site is dedicated to helping you solve algebra problems.
The Basic Logic through Pictures, is an introduction to some fundamental ideas of classical logic with interactive illustrations.
The Introduction to Proofs page is a good first step toward reading Prooftoys proofs and building your own.
There is quite a bit more yet to be said about the logic as well. Fortunately the logic and inference steps are quite standard, so any part that looks familiar should work for you in textbook fashion.
In the web-based Proof Builder user interface you can select steps, expressions, and locations in steps by pointing and clicking, and apply any predefined or extended public inference rule. When reading an existing proof you can drill down into the details of high-level inference steps or theorems to see how they are proved in more detail.
The engine implements a variant of Professor Peter B. Andrews' Q0, a version of higher-order logic with a small, simple, and understandable kernel. On this base it builds natural deduction-style reasoning and a variety high-level inference rules that make it easy to build high-level proofs.
The engine is safely programmable, and you can create new high-level inference rules without compromising correctness.
The Proof builder is also available on a standalone page.
Note: Proof displays and the proof builder are supported in recent versions of Firefox and Chrome.
An Introduction to Mathematical Logic and Type Theory by Professor Andrews contains a rigorous presentation of the full logic implemented here among other logical topics.