Theorem r19.29r 3073

Description: Restricted quantifier version of 19.29r 1802; variation of r19.29 3072. (Contributed by NM, 31-Aug-1999.)

Assertion

Ref	Expression
r19.29r	|- ( ( E. x e. A ph /\ A. x e. A ps ) -> E. x e. A ( ph /\ ps ) )

Proof of Theorem r19.29r

Step	Hyp	Ref	Expression
1		r19.29 3072	. 2 |- ( ( A. x e. A ps /\ E. x e. A ph ) -> E. x e. A ( ps /\ ph ) )
2		ancom 466	. 2 |- ( ( E. x e. A ph /\ A. x e. A ps ) <-> ( A. x e. A ps /\ E. x e. A ph ) )
3		ancom 466	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
4	3	rexbii 3041	. 2 |- ( E. x e. A ( ph /\ ps ) <-> E. x e. A ( ps /\ ph ) )
5	1, 2, 4	3imtr4i 281	1 |- ( ( E. x e. A ph /\ A. x e. A ps ) -> E. x e. A ( ph /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 384   A.wral 2912   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  r19.29imd  3074  2reu5  3416  rlimuni  14281  rlimno1  14384  neindisj2  20927  lmss  21102  fclsbas  21825  isfcf  21838  ucnima  22085  metcnp3  22345  cfilucfil  22364  bndth  22757  ellimc3  23643  lmxrge0  29998  gsumesum  30121  esumcst  30125  esumfsup  30132  voliune  30292  volfiniune  30293  bnj517  30955  cover2  33508  prmunb2  38510