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 | ⊢ ( ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | wph | ⊢ 𝜑 | |
| 2 | 1 0 | wal | ⊢ ∀ 𝑥 𝜑 |
| 3 | wps | ⊢ 𝜓 | |
| 4 | 2 3 | wi | ⊢ ( ∀ 𝑥 𝜑 → 𝜓 ) |
| 5 | 4 0 | wal | ⊢ ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) |
| 6 | 3 0 | wal | ⊢ ∀ 𝑥 𝜓 |
| 7 | 2 6 | wi | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) |
| 8 | 5 7 | wi | ⊢ ( ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) |