Theorem bj-nfalt

Description: Closed form of nfal . (Contributed by BJ, 2-May-2019)

	Ref	Expression
Assertion	bj-nfalt	|- ( A. x F/ y ph -> F/ y A. x ph )

Proof

Step	Hyp	Ref	Expression
1		bj-hbalt	|- ( A. x ( ph -> A. y ph ) -> ( A. x ph -> A. y A. x ph ) )
2	1	alimi	|- ( A. y A. x ( ph -> A. y ph ) -> A. y ( A. x ph -> A. y A. x ph ) )
3	2	alcoms	|- ( A. x A. y ( ph -> A. y ph ) -> A. y ( A. x ph -> A. y A. x ph ) )
4		nf5	|- ( F/ y ph <-> A. y ( ph -> A. y ph ) )
5	4	albii	|- ( A. x F/ y ph <-> A. x A. y ( ph -> A. y ph ) )
6		nf5	|- ( F/ y A. x ph <-> A. y ( A. x ph -> A. y A. x ph ) )
7	3 5 6	3imtr4i	|- ( A. x F/ y ph -> F/ y A. x ph )