Theorem ralimia 2527

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

Syntax hints:   -> wi 4   e. wcel 2136   A.wral 2444

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 1435  ax-gen 1437

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

This theorem is referenced by:  ralimiaa  2528  ralimi  2529  r19.12  2572  rr19.3v  2865  rr19.28v  2866  ffvresb  5648  f1mpt  5739  ixpf  6686  exmidontri2or  7199  peano2nnnn  7794  peano5nnnn  7833  peano5nni  8860  peano2nn  8869  serf0  11293  baspartn  12688  tridceq  13935