Description: The setvar x is not free in A. x ph . Example in Appendix in Megill p. 450 (p. 19 of the preprint). Also Lemma 22 of Monk2 p. 114. (Contributed by NM, 24-Jan-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hba1-o | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-c5 | ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → ¬ ∀ 𝑥 𝜑 ) | |
| 2 | 1 | con2i | ⊢ ( ∀ 𝑥 𝜑 → ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) |
| 3 | ax10fromc7 | ⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) | |
| 4 | ax10fromc7 | ⊢ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) | |
| 5 | 4 | con1i | ⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) |
| 6 | 5 | alimi | ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 ) |
| 7 | 2 3 6 | 3syl | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 ) |