Theorem r19.35OLD

Description: Obsolete version of 19.35 as of 22-Dec-2024. (Contributed by NM, 20-Sep-2003) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	r19.35OLD	|- ( E. x e. A ( ph -> ps ) <-> ( A. x e. A ph -> E. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		rexim	|- ( A. x e. A ( ( ph -> ps ) -> ps ) -> ( E. x e. A ( ph -> ps ) -> E. x e. A ps ) )
2		pm2.27	|- ( ph -> ( ( ph -> ps ) -> ps ) )
3	2	ralimi	|- ( A. x e. A ph -> A. x e. A ( ( ph -> ps ) -> ps ) )
4	1 3	syl11	|- ( E. x e. A ( ph -> ps ) -> ( A. x e. A ph -> E. x e. A ps ) )
5		rexnal	|- ( E. x e. A -. ph <-> -. A. x e. A ph )
6		pm2.21	|- ( -. ph -> ( ph -> ps ) )
7	6	reximi	|- ( E. x e. A -. ph -> E. x e. A ( ph -> ps ) )
8	5 7	sylbir	|- ( -. A. x e. A ph -> E. x e. A ( ph -> ps ) )
9		ax-1	|- ( ps -> ( ph -> ps ) )
10	9	reximi	|- ( E. x e. A ps -> E. x e. A ( ph -> ps ) )
11	8 10	ja	|- ( ( A. x e. A ph -> E. x e. A ps ) -> E. x e. A ( ph -> ps ) )
12	4 11	impbii	|- ( E. x e. A ( ph -> ps ) <-> ( A. x e. A ph -> E. x e. A ps ) )