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
|- F/ y ph
nfald.2
|- ( ph -> F/ x ps )
Assertion nfald
|- ( ph -> F/ x A. y ps )

Proof

Step Hyp Ref Expression
1 nfald.1
 |-  F/ y ph
2 nfald.2
 |-  ( ph -> F/ x ps )
3 19.12
 |-  ( E. x A. y ps -> A. y E. x ps )
4 2 nfrd
 |-  ( ph -> ( E. x ps -> A. x ps ) )
5 1 4 alimd
 |-  ( ph -> ( A. y E. x ps -> A. y A. x ps ) )
6 ax-11
 |-  ( A. y A. x ps -> A. x A. y ps )
7 3 5 6 syl56
 |-  ( ph -> ( E. x A. y ps -> A. x A. y ps ) )
8 7 nfd
 |-  ( ph -> F/ x A. y ps )