Theorem ralimia 2558

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

Syntax hints:   -> wi 4   e. wcel 2167   A.wral 2475

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 1461  ax-gen 1463

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

This theorem is referenced by:  ralimiaa  2559  ralimi  2560  r19.12  2603  rr19.3v  2903  rr19.28v  2904  ffvresb  5726  f1mpt  5819  ixpf  6780  exmidontri2or  7312  peano2nnnn  7922  peano5nnnn  7961  peano5nni  8995  peano2nn  9004  serf0  11519  baspartn  14296  tridceq  15710