Theorem ralimiaa 2951

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
ralimiaa.1	|- ( ( x e. A /\ ph ) -> ps )

Assertion

Ref	Expression
ralimiaa	|- ( A. x e. A ph -> A. x e. A ps )

Proof of Theorem ralimiaa

Step	Hyp	Ref	Expression
1		ralimiaa.1	. . 3 |- ( ( x e. A /\ ph ) -> ps )
2	1	ex 450	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	ralimia 2950	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

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-ral 2917

This theorem is referenced by:  ralrnmpt  6368  tz7.48-2  7537  mptelixpg  7945  boxriin  7950  acnlem  8871  iundom2g  9362  konigthlem  9390  hashge2el2dif  13262  rlim2  14227  prdsbas3  16141  prdsdsval2  16144  ptbasfi  21384  ptunimpt  21398  voliun  23322  lgamgulmlem6  24760  riesz4i  28922  dmdbr6ati  29282