Theorem 19.26

Description: Theorem 19.26 of Margaris p. 90. Also Theorem *10.22 of WhiteheadRussell p. 147. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 4-Jul-2014)

	Ref	Expression
Assertion	19.26	|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( ph /\ ps ) -> ph )
2	1	alimi	|- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr	|- ( ( ph /\ ps ) -> ps )
4	3	alimi	|- ( A. x ( ph /\ ps ) -> A. x ps )
5	2 4	jca	|- ( A. x ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) )
6		id	|- ( ( ph /\ ps ) -> ( ph /\ ps ) )
7	6	alanimi	|- ( ( A. x ph /\ A. x ps ) -> A. x ( ph /\ ps ) )
8	5 7	impbii	|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )