Theorem ralimi 2613

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 2611	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:  2ralimi  2614  ral2imi  2615  r19.26  2677  r19.29  2688  rr19.3v  2965  rr19.28v  2966  reu3  3016  uniiunlem  3338  reupick2  3519  rabxmdc  3554  uniss2  3966  ss2iun  4027  iineq2  4029  iunss2  4057  disjss2  4109  disjeq2  4110  disjnim  4120  repizf  4247  abnexg  4592  reusv3i  4605  tfis  4730  ssrel2  4865  issref  5170  dmmptg  5285  funco  5417  fununi  5449  fun11uni  5451  funimaexglem  5464  fnmpt  5510  fun11iun  5660  mpteqb  5796  chfnrn  5820  dffo5  5857  ffvresb  5871  fmptcof  5875  dfmptg  5888  mpo2eqb  6198  ralrnmpo  6203  rexrnmpo  6204  uchoice  6371  fnmpo  6438  mpoexxg  6446  smores  6563  riinerm  6882  ixpm  7012  difinfinf  7441  nninfwlpoimlemginf  7516  exmidontriimlem1  7577  onntri13  7597  onntri24  7601  cc4f  7635  cc4n  7637  cauappcvgprlemdisj  8018  caucvgsrlemasr  8157  caucvgsr  8169  suplocsr  8176  rexuz3  11770  recvguniq  11775  cau3lem  11895  caubnd2  11898  rexanre  12001  climi2  12070  climi0  12071  climcaucn  12133  ndvdssub  12713  gcdsupex  12750  gcdsupcl  12751  bezoutlemmo  12799  ptex  13667  mgmidmo  13741  issubg2m  14041  eltg2b  15204  neipsm  15304  lmcvg  15367  txlm  15429  metrest  15656  mulcncflem  15757  wlkvtxeledgg  16683  upgrwlkcompim  16701  upgrwlkvtxedg  16703  upgr2wlkdc  16716  bj-charfunbi  16935  bj-indint  17055  bj-indind  17056  bj-bdfindis  17071  setindis  17091  bdsetindis  17093  pw1dceq  17133  exmidcon  17135  exmidpeirce  17136  neap0mkv  17217