Theorem ralimia 2611

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  ralimiaa  2612  ralimi  2613  r19.12  2657  rr19.3v  2965  rr19.28v  2966  ffvresb  5871  f1mpt  5977  ixpf  7002  exmidontri2or  7602  peano2nnnn  8220  peano5nnnn  8259  peano5nni  9307  peano2nn  9316  serf0  12118  baspartn  15151  tridceq  17106