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 ψ