This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfa2

Description: Lemma 24 of Monk2 p. 114. (Contributed by Mario Carneiro, 24-Sep-2016) Remove dependency on ax-12 . (Revised by Wolf Lammen, 18-Oct-2021)

		Ref	Expression
	Assertion	nfa2	⊢ Ⅎ 𝑥 ∀ 𝑦 ∀ 𝑥 𝜑

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑦 ∀ 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 𝜑 )
2		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∀ 𝑦 𝜑
3	1 2	nfxfr	⊢ Ⅎ 𝑥 ∀ 𝑦 ∀ 𝑥 𝜑