Theorem hba1

Description: The setvar x is not free in A. x ph . This corresponds to the axiom (4) of modal logic. 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 shortened by Wolf Lammen, 12-Oct-2021)

	Ref	Expression
Assertion	hba1	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝜑
2	1	nf5ri	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 )