Theorem ralimia 2518

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

Syntax hints:   -> wi 4   e. wcel 2128   A.wral 2435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429

This theorem depends on definitions:  df-bi 116  df-ral 2440

This theorem is referenced by:  ralimiaa  2519  ralimi  2520  r19.12  2563  rr19.3v  2851  rr19.28v  2852  ffvresb  5627  f1mpt  5716  ixpf  6658  exmidontri2or  7161  peano2nnnn  7756  peano5nnnn  7795  peano5nni  8819  peano2nn  8828  serf0  11231  baspartn  12408  tridceq  13590