Substitution of Proof Lines

Description

Uses the following modules:

• propaxiom_1.00.00_1.00.00.html
• predaxiom_1.00.00_1.00.00.html

Is used by the following modules:

• prophilbert1_1.00.00_1.02.00.html

If a proof line could be derived by using rename proposition variable, rename bound subject variable, rename free subject variable and replace predicate variable multiple times, we declare a new rule to shorten that derivation:

1 Rule Declaration
      Substitute Variables     (rule8)

The use of this rule could always be replaced by proof lines that make only use of the referenced rules.