Theorem r19.26 2632

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 109	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	ralimi 2569	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2569	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 306	. 2 |- ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6		pm3.2 139	. . . 4 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	ral2imi 2571	. . 3 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8	7	imp 124	. 2 |- ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9	5, 8	impbii 126	1 |- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   A.wral 2484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472

This theorem depends on definitions:  df-bi 117  df-ral 2489

This theorem is referenced by:  r19.27v  2633  r19.28v  2634  r19.26-2  2635  r19.26-3  2636  ralbiim  2640  r19.27av  2641  reu8  2969  ssrab  3271  r19.28m  3550  r19.27m  3556  2ralunsn  3839  iuneq2  3943  cnvpom  5225  funco  5311  fncnv  5340  funimaexglem  5357  fnres  5392  fnopabg  5399  mpteqb  5670  eqfnfv3  5679  caoftrn  6191  iinerm  6694  ixpeq2  6799  ixpin  6810  rexanuz  11299  recvguniq  11306  cau3lem  11425  rexanre  11531  bezoutlemmo  12327  sqrt2irr  12484  pc11  12654  issubg3  13528  issubg4m  13529  ringsrg  13809  tgval2  14523  metequiv  14967  metequiv2  14968  mulcncflem  15079  2sqlem6  15597  bj-indind  15872