Theorem albi

Description: Theorem 19.15 of Margaris p. 90. (Contributed by NM, 24-Jan-1993)

	Ref	Expression
Assertion	albi	|- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )
2	1	al2imi	|- ( A. x ( ph <-> ps ) -> ( A. x ph -> A. x ps ) )
3		biimpr	|- ( ( ph <-> ps ) -> ( ps -> ph ) )
4	3	al2imi	|- ( A. x ( ph <-> ps ) -> ( A. x ps -> A. x ph ) )
5	2 4	impbid	|- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )