Theorem bj-19.23t

Description: Statement 19.23t proved from modalK (obsoleting 19.23v ). (Contributed by BJ, 2-Dec-2023)

	Ref	Expression
Assertion	bj-19.23t	|- ( F// x ps -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnf-exlim	|- ( F// x ps -> ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) ) )
2		bj-nnfa	|- ( F// x ps -> ( ps -> A. x ps ) )
3	2	imim2d	|- ( F// x ps -> ( ( E. x ph -> ps ) -> ( E. x ph -> A. x ps ) ) )
4		19.38	|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
5	3 4	syl6	|- ( F// x ps -> ( ( E. x ph -> ps ) -> A. x ( ph -> ps ) ) )
6	1 5	impbid	|- ( F// x ps -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )