Theorem 19.17

Description: Theorem 19.17 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)

	Ref	Expression
Hypothesis	19.17.1	|- F/ x ps
Assertion	19.17	|- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.17.1	|- F/ x ps
2		albi	|- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
3	1	19.3	|- ( A. x ps <-> ps )
4	2 3	bitrdi	|- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) )