**Description: **Axiom of Quantified
Implication. This axiom moves a quantifier from
outside to inside an implication, quantifying . Notice that
must not be a free variable in the antecedent of the quantified
implication, and we express this by binding to "protect" the axiom
from a
containing a free .
One of the 4 axioms of "pure"
predicate calculus. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the
preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5
of [Mendelson] p. 69.
This axiom is redundant, as shown by theorem ax5o 1693.
Normally, ax5o 1693 should be used rather than ax-5o 1694, except by theorems
specifically studying the latter's properties. (Contributed by NM,
5-Aug-1993.) (New usage is discouraged.) |