Theorem ralimia 2555

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

Syntax hints:   -> wi 4   e. wcel 2164   A.wral 2472

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 1458  ax-gen 1460

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

This theorem is referenced by:  ralimiaa  2556  ralimi  2557  r19.12  2600  rr19.3v  2899  rr19.28v  2900  ffvresb  5721  f1mpt  5814  ixpf  6774  exmidontri2or  7303  peano2nnnn  7913  peano5nnnn  7952  peano5nni  8985  peano2nn  8994  serf0  11495  baspartn  14218  tridceq  15546