Theorem ralimi 2427

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	|- ( ph -> ps )

Assertion

Ref	Expression
ralimi	|- ( A. x e. A ph -> A. x e. A ps )

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 |- ( ph -> ps )
2	1	a1i 9	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	ralimia 2425	1 |- ( A. x e. A ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1434   A.wral 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379

This theorem depends on definitions:  df-bi 115  df-ral 2354

This theorem is referenced by:  ral2imi  2428  r19.26  2486  r19.29  2495  rr19.3v  2734  rr19.28v  2735  reu3  2783  uniiunlem  3083  reupick2  3257  uniss2  3640  ss2iun  3701  iineq2  3703  iunss2  3731  disjss2  3777  disjeq2  3778  repizf  3902  reusv3i  4217  tfis  4332  ssrel2  4456  issref  4737  dmmptg  4848  funco  4970  fununi  4998  fun11uni  5000  funimaexglem  5013  fnmpt  5056  fun11iun  5178  mpteqb  5293  chfnrn  5310  dffo5  5348  ffvresb  5360  fmptcof  5363  dfmptg  5374  mpt22eqb  5641  ralrnmpt2  5646  rexrnmpt2  5647  fnmpt2  5859  mpt2exxg  5864  smores  5941  riinerm  6245  cauappcvgprlemdisj  6903  caucvgsrlemasr  7028  caucvgsr  7040  rexuz3  10014  recvguniq  10019  cau3lem  10138  caubnd2  10141  rexanre  10244  climi2  10265  climi0  10266  climcaucn  10326  ndvdssub  10474  gcdsupex  10493  gcdsupcl  10494  bezoutlemmo  10539  bj-indint  10884  bj-indind  10885  bj-bdfindis  10900  setindis  10920  bdsetindis  10922