Derived Rules of Logic E

I assume you know that we now work with 4 (not 3) inference rules. The
three in the text are Substitution, Transitivity, and Leibniz. The new
one is Equanimity:
                P, P == Q
  Equanimity: ------------
                  Q
With this additional rule, a theorem can be defined as traditionally
done in logic: a theorem is (0) an axiom or (1) the conclusion of an
inference rule whose premises are theorems.
Here is an example of the use of Equanimity, in proving that p==p is a
theorem.
      p == p
  =    <Symmetry, p  ==  q == q == p, with q:= p,
        (to replace the second p of p == p)>
      p == p == p == p    ---Symmetry of ==
In the above, the statement "---Symmetry of ==" on the last line
indicates that the last formula is a theorem and that Equanimity
should be used to conclude that the first line is a theorem.
======================================
The next edition of our text is likely to have four derived inference
rules.
                         P
  Redundant true:    --------
                     P == true
This rule is used as follows in a proof. Suppose we know that P is a
theorem. Then a step may be written as, for example,
     P \/ Q
 =     <Redundant true: P>
     true \/ Q

                  P, P => Q
  Modus ponens   ----------
                     Q
This rule is used can be used in a weakening proof as in the following
example. Suppose P is a known theorem, say theorem (20).
     P    --- (20)
 =    <hint>
     P1
 =>   <hint>
     P2
 =    <hint>
     Q
The indication on the first line that P is a theorem alerts the reader
to the fact that the last line Q is a theorem, by inference rule Modus
Ponens.

The next two inference rules deal with Monotonicity, suppose a
variable z occurs exactly once in an expression E, and not in an
operand of an equivalence (or inequivalence). Let n be the number of
negations, antecedents of implications, and ranges of universal
quantifications in which z appears. The parity of the position of x is
even if n is even and is odd if n is odd.
Examples:
     E                     n    parity of z in E
   x \/ z                  0     even
   \neg (x \/ z)           1     odd
   (\neg x) => z           0     even
   (\neg z) => x           2     even
   (A x| \neg z \/ x: P)   2     even
   (A x| z \/ x: P)        1     odd


                           P => Q
    Monotonicity:      --------------     (parity of z in E is even)
                       E[z:=P] => E[z:=Q]


                           P => Q
    Antimonotonicity:   --------------     (parity of z in E is odd)
                       E[z:=P] <= E[z:=Q]

Here is a use of each:

     R => P
  =>   <Monotonicity: Weakening, p => p \/ q>
     R => (p \/ q)

     P => R
  =>   <Antimonotonicity: Weakening, p => p \/ q>
     (p \/ q) => R

Inference rule Redundant true and the monotonicity inference rules
need to be named when they are used, to alert the reader to their use.
THe other inference rules need not be named because their use is
indicated by the proof itself.

How about also adding the following derived rule:

		        P, Q
                ------------------      (TR = theorem replacement)
		E[z:=P] == E[z:=Q]