Theorem bj-ceqsalt0

Description: The FOL content of ceqsalt . Lemma for bj-ceqsalt and bj-ceqsaltv . (Contributed by BJ, 26-Sep-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ceqsalt0	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( th -> ph ) <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> E. x th )
2		biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )
3	2	imim3i	|- ( ( th -> ( ph <-> ps ) ) -> ( ( th -> ph ) -> ( th -> ps ) ) )
4	3	al2imi	|- ( A. x ( th -> ( ph <-> ps ) ) -> ( A. x ( th -> ph ) -> A. x ( th -> ps ) ) )
5	4	3ad2ant2	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( th -> ph ) -> A. x ( th -> ps ) ) )
6		19.23t	|- ( F/ x ps -> ( A. x ( th -> ps ) <-> ( E. x th -> ps ) ) )
7	6	3ad2ant1	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( th -> ps ) <-> ( E. x th -> ps ) ) )
8	5 7	sylibd	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( th -> ph ) -> ( E. x th -> ps ) ) )
9	1 8	mpid	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( th -> ph ) -> ps ) )
10		biimpr	|- ( ( ph <-> ps ) -> ( ps -> ph ) )
11	10	imim2i	|- ( ( th -> ( ph <-> ps ) ) -> ( th -> ( ps -> ph ) ) )
12	11	com23	|- ( ( th -> ( ph <-> ps ) ) -> ( ps -> ( th -> ph ) ) )
13	12	alimi	|- ( A. x ( th -> ( ph <-> ps ) ) -> A. x ( ps -> ( th -> ph ) ) )
14	13	3ad2ant2	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> A. x ( ps -> ( th -> ph ) ) )
15		19.21t	|- ( F/ x ps -> ( A. x ( ps -> ( th -> ph ) ) <-> ( ps -> A. x ( th -> ph ) ) ) )
16	15	3ad2ant1	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( ps -> ( th -> ph ) ) <-> ( ps -> A. x ( th -> ph ) ) ) )
17	14 16	mpbid	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( ps -> A. x ( th -> ph ) ) )
18	9 17	impbid	|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( th -> ph ) <-> ps ) )