Theorem ralimia 2591

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)

Hypothesis

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

Assertion

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

Proof of Theorem ralimia

Step	Hyp	Ref	Expression
1		ralimia.1	. . 3 |- ( x e. A -> ( ph -> ps ) )
2	1	a2i 11	. 2 |- ( ( x e. A -> ph ) -> ( x e. A -> ps ) )
3	2	ralimi2 2590	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495

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

This theorem is referenced by:  ralimiaa  2592  ralimi  2593  r19.12  2637  rr19.3v  2942  rr19.28v  2943  ffvresb  5800  f1mpt  5901  ixpf  6875  exmidontri2or  7439  peano2nnnn  8051  peano5nnnn  8090  peano5nni  9124  peano2nn  9133  serf0  11879  baspartn  14740  tridceq  16512