Theorem ralimia 2548

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

Syntax hints:   -> wi 4   e. wcel 2158   A.wral 2465

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 1457  ax-gen 1459

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

This theorem is referenced by:  ralimiaa  2549  ralimi  2550  r19.12  2593  rr19.3v  2888  rr19.28v  2889  ffvresb  5692  f1mpt  5785  ixpf  6734  exmidontri2or  7256  peano2nnnn  7866  peano5nnnn  7905  peano5nni  8936  peano2nn  8945  serf0  11374  baspartn  13846  tridceq  15101