Theorem bj-cbv3ta

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

	Ref	Expression
Assertion	bj-cbv3ta	|- ( A. x A. y ( x = y -> ( ph -> ps ) ) -> ( ( A. y ( E. x ps -> ps ) /\ A. x ( ph -> A. y ph ) ) -> ( A. x ph -> A. y ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-spimt2	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( ( E. x ps -> ps ) -> ( A. x ph -> ps ) ) )
2	1	imp	|- ( ( A. x ( x = y -> ( ph -> ps ) ) /\ ( E. x ps -> ps ) ) -> ( A. x ph -> ps ) )
3	2	alanimi	|- ( ( A. y A. x ( x = y -> ( ph -> ps ) ) /\ A. y ( E. x ps -> ps ) ) -> A. y ( A. x ph -> ps ) )
4		bj-hbalt	|- ( A. x ( ph -> A. y ph ) -> ( A. x ph -> A. y A. x ph ) )
5		sylgt	|- ( A. y ( A. x ph -> ps ) -> ( ( A. x ph -> A. y A. x ph ) -> ( A. x ph -> A. y ps ) ) )
6	3 4 5	syl2im	|- ( ( A. y A. x ( x = y -> ( ph -> ps ) ) /\ A. y ( E. x ps -> ps ) ) -> ( A. x ( ph -> A. y ph ) -> ( A. x ph -> A. y ps ) ) )
7	6	expimpd	|- ( A. y A. x ( x = y -> ( ph -> ps ) ) -> ( ( A. y ( E. x ps -> ps ) /\ A. x ( ph -> A. y ph ) ) -> ( A. x ph -> A. y ps ) ) )
8	7	alcoms	|- ( A. x A. y ( x = y -> ( ph -> ps ) ) -> ( ( A. y ( E. x ps -> ps ) /\ A. x ( ph -> A. y ph ) ) -> ( A. x ph -> A. y ps ) ) )