Description: Axiom of Quantified Implication. This axiom moves a universal quantifier from outside to inside an implication, quantifying ps . Notice that x must not be a free variable in the antecedent of the quantified implication, and we express this by binding ph to "protect" the axiom from a ph containing a free x . 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 obsolete and should no longer be used. It is proved above as Theorem axc4 . (Contributed by NM, 3-Jan-1993) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-c4 | |- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | wph | |- ph |
|
| 2 | 1 0 | wal | |- A. x ph |
| 3 | wps | |- ps |
|
| 4 | 2 3 | wi | |- ( A. x ph -> ps ) |
| 5 | 4 0 | wal | |- A. x ( A. x ph -> ps ) |
| 6 | 3 0 | wal | |- A. x ps |
| 7 | 2 6 | wi | |- ( A. x ph -> A. x ps ) |
| 8 | 5 7 | wi | |- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) ) |