Theorem 19.27

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

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

Proof

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