Theorem ralimia 2569

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 2568	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 2178   A.wral 2486

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 1471  ax-gen 1473

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

This theorem is referenced by:  ralimiaa  2570  ralimi  2571  r19.12  2614  rr19.3v  2919  rr19.28v  2920  ffvresb  5766  f1mpt  5863  ixpf  6830  exmidontri2or  7389  peano2nnnn  8001  peano5nnnn  8040  peano5nni  9074  peano2nn  9083  serf0  11778  baspartn  14637  tridceq  16197