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 <a href="propaxiom ₁ .00.00 ₁ .00.00.html#rule4">rename proposition variable</a>, <a href="predaxiom ₁ .00.00 ₁ .00.00.html#predrule1">rename bound subject variable</a> and <a href="predaxiom ₁ .00.00 ₁ .00.00.html#predrule2">rename free subject variable</a> 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.

This module is used by the following modules:

• prophilbert1_1.00.00_1.02.00.html