Operator priority : (high)
| Proof Line
||adds A to the end of the list
of the hypothesis of the previous proof line
|| no conditions
therefore A => B.
||removes the last introduced hypothesis.
This proof line is the application of the rule =>I
The removed hypothesis must be A.
The formula B must be usable on the previous proof line.
|| no effects
||The formula A must be a copy of a formula usable
on this proof line or must be obtained by application of a
rule to formulas usable on this line.