Theorem bj-ceqsalt1

Description: The FOL content of ceqsalt . Lemma for bj-ceqsalt and bj-ceqsaltv . TODO: consider removing if it does not add anything to bj-ceqsalt0 . (Contributed by BJ, 26-Sep-2019) (Proof modification is discouraged.)

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

Proof

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