Theorem ralimia 2817

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 13	. 2 |- ( ( x e. A -> ph ) -> ( x e. A -> ps ) )
3	2	ralimi2 2816	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1758   A.wral 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603

This theorem depends on definitions:  df-bi 185  df-ral 2804

This theorem is referenced by:  ralimiaa  2818  ralimi  2819  r19.12  2936  rr19.3v  3208  rr19.28v  3209  exfo  5971  ffvresb  5984  f1mpt  6084  weniso  6155  ixpf  7396  ixpiunwdom  7918  tz9.12lem3  8108  dfac2a  8411  kmlem12  8442  axdc2lem  8729  ac6num  8760  ac6c4  8762  brdom6disj  8811  konigthlem  8844  arch  10688  cshw1  12575  serf0  13277  symgextfo  16047  baspartn  18692  ptcnplem  19327  rngmgmbs4  24057  spanuni  25100  lnopunilem1  25567  finixpnum  28563  indexa  28776  heiborlem5  28863  mzpincl  29219  dfac11  29564