The rules like introduction and elimination are not to allow you writing anything you want, but to help you using or creating a formula with a concrete operator.

That's why, if you have , you can't say ``now I do negation introduction and get , which is what I needed''. There are some requisites for each rule, and if you don't fulfill them, you can't apply that rule.

For instance: the rule implication elimination doesn't allow to use the formulas in the first line this way:

To be able to do this, we would need to be sure that is always true; then we could apply the rule, correctly writing the line numbers.

Daniel Clemente Laboreo 2005-05-17