Theorem 19.28

Description: Theorem 19.28 of Margaris p. 90. See 19.28v for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993)

	Ref	Expression
Hypothesis	19.28.1	|- F/ x ph
Assertion	19.28	|- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.28.1	|- F/ x ph
2		19.26	|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )
3	1	19.3	|- ( A. x ph <-> ph )
4	3	anbi1i	|- ( ( A. x ph /\ A. x ps ) <-> ( ph /\ A. x ps ) )
5	2 4	bitri	|- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )