This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )