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

Metamath Proof Explorer

Theorem nfald

Description: Deduction form of nfal . (Contributed by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 16-Oct-2021)

Ref Expression
Hypotheses nfald.1 ⊢ Ⅎ y φ
nfald.2 ⊢ φ → Ⅎ x ψ
Assertion nfald ⊢ φ → Ⅎ x ∀ y ψ

Proof

Step Hyp Ref Expression
1 nfald.1 ⊢ Ⅎ y φ
2 nfald.2 ⊢ φ → Ⅎ x ψ
3 19.12 ⊢ ∃ x ∀ y ψ → ∀ y ∃ x ψ
4 2 nfrd ⊢ φ → ∃ x ψ → ∀ x ψ
5 1 4 alimd ⊢ φ → ∀ y ∃ x ψ → ∀ y ∀ x ψ
6 ax-11 ⊢ ∀ y ∀ x ψ → ∀ x ∀ y ψ
7 3 5 6 syl56 ⊢ φ → ∃ x ∀ y ψ → ∀ x ∀ y ψ
8 7 nfd ⊢ φ → Ⅎ x ∀ y ψ