Theorem ralimia 2855

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

Syntax hints:   -> wi 4   e. wcel 1767   A.wral 2814

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

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

This theorem is referenced by:  ralimiaa  2856  ralimi  2857  r19.12  2988  rr19.3v  3245  rr19.28v  3246  exfo  6037  ffvresb  6050  f1mpt  6155  weniso  6236  ixpf  7488  ixpiunwdom  8013  tz9.12lem3  8203  dfac2a  8506  kmlem12  8537  axdc2lem  8824  ac6num  8855  ac6c4  8857  brdom6disj  8906  konigthlem  8939  arch  10788  cshw1  12747  serf0  13459  symgextfo  16239  baspartn  19219  ptcnplem  19854  rngmgmbs4  25092  spanuni  26135  lnopunilem1  26602  finixpnum  29612  indexa  29825  heiborlem5  29912  mzpincl  30268  dfac11  30612