Theorem r19.26 2486

Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
r19.26	|- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Proof of Theorem r19.26

Step	Hyp	Ref	Expression
1		simpl 107	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	ralimi 2427	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 108	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2427	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 300	. 2 |- ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6		pm3.2 137	. . . 4 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	ral2imi 2428	. . 3 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8	7	imp 122	. 2 |- ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9	5, 8	impbii 124	1 |- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Syntax hints:   /\ wa 102   <-> wb 103   A.wral 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379

This theorem depends on definitions:  df-bi 115  df-ral 2354

This theorem is referenced by:  r19.26-2  2487  r19.26-3  2488  ralbiim  2492  r19.27av  2493  reu8  2789  ssrab  3073  r19.28m  3338  r19.27m  3344  2ralunsn  3598  iuneq2  3702  cnvpom  4890  funco  4970  fncnv  4996  funimaexglem  5013  fnres  5046  fnopabg  5053  mpteqb  5293  eqfnfv3  5299  caoftrn  5767  iinerm  6244  rexanuz  10012  recvguniq  10019  cau3lem  10138  rexanre  10244  bezoutlemmo  10539  sqrt2irr  10685  bj-indind  10885