Theorem bj-pm11.53vw

Description: Version of pm11.53v with nonfreeness antecedents. One can also prove the theorem with antecedent ( F// y A. x ph /\ A. y F// x ps ) . (Contributed by BJ, 7-Oct-2024)

	Ref	Expression
Assertion	bj-pm11.53vw	|- ( ( A. x F// y ph /\ F// x A. y ps ) -> ( A. x A. y ( ph -> ps ) <-> ( E. x ph -> A. y ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A. x F// y ph /\ F// x A. y ps ) -> A. x F// y ph )
2		bj-19.21t	|- ( F// y ph -> ( A. y ( ph -> ps ) <-> ( ph -> A. y ps ) ) )
3	1 2	sylg	|- ( ( A. x F// y ph /\ F// x A. y ps ) -> A. x ( A. y ( ph -> ps ) <-> ( ph -> A. y ps ) ) )
4		albi	|- ( A. x ( A. y ( ph -> ps ) <-> ( ph -> A. y ps ) ) -> ( A. x A. y ( ph -> ps ) <-> A. x ( ph -> A. y ps ) ) )
5	3 4	syl	|- ( ( A. x F// y ph /\ F// x A. y ps ) -> ( A. x A. y ( ph -> ps ) <-> A. x ( ph -> A. y ps ) ) )
6		bj-19.23t	|- ( F// x A. y ps -> ( A. x ( ph -> A. y ps ) <-> ( E. x ph -> A. y ps ) ) )
7	6	adantl	|- ( ( A. x F// y ph /\ F// x A. y ps ) -> ( A. x ( ph -> A. y ps ) <-> ( E. x ph -> A. y ps ) ) )
8	5 7	bitrd	|- ( ( A. x F// y ph /\ F// x A. y ps ) -> ( A. x A. y ( ph -> ps ) <-> ( E. x ph -> A. y ps ) ) )