a formal proof is a finite sequence of premises each of which is an axiom, an assumption, or follows from the preceding statements in the sequence by a rule of inference, which are used to prove arguments.
a proof sequence from to a proposition is one such that is the last proposition in the sequence which we call the conclusion. we write
usually, on the right side of each formula we write a description of how it was derived and from which previous lines in the inference process
correct use of equivalences and implications
use of equivalences can also be done on subformulas
use of logical implications cannot be done on subformulas, only on full rows during the formal proof
an example of incorrect usage: