Metamath Proof Explorer


Theorem nfal

Description: If x is not free in ph , it is not free in A. y ph . (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypothesis nfal.1 x φ
Assertion nfal x y φ

Proof

Step Hyp Ref Expression
1 nfal.1 x φ
2 1 nf5ri φ x φ
3 2 hbal y φ x y φ
4 3 nf5i x y φ