Theorem ralimia 2795

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

Syntax hints:   -> wi 4   e. wcel 1842   A.wral 2754

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

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

This theorem is referenced by:  ralimiaa  2796  ralimi  2797  r19.12  2933  rr19.3v  3191  rr19.28v  3192  exfo  6027  ffvresb  6041  f1mpt  6150  weniso  6233  ixpf  7529  ixpiunwdom  8051  tz9.12lem3  8239  dfac2a  8542  kmlem12  8573  axdc2lem  8860  ac6num  8891  ac6c4  8893  brdom6disj  8942  konigthlem  8975  arch  10833  cshw1  12846  serf0  13652  symgextfo  16771  baspartn  19747  ptcnplem  20414  rngmgmbs4  25833  spanuni  26876  lnopunilem1  27342  finixpnum  31410  indexa  31506  heiborlem5  31593  mzpincl  35028  dfac11  35370  stgoldbwt  37830  2zrngnmlid2  38268