Theorem ralimi 2596

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

Syntax hints:   -> wi 4   e. wcel 2202   A.wral 2511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117  df-ral 2516

This theorem is referenced by:  2ralimi  2597  ral2imi  2598  r19.26  2660  r19.29  2671  rr19.3v  2946  rr19.28v  2947  reu3  2997  uniiunlem  3318  reupick2  3495  uniss2  3929  ss2iun  3990  iineq2  3992  iunss2  4020  disjss2  4072  disjeq2  4073  disjnim  4083  repizf  4210  abnexg  4549  reusv3i  4562  tfis  4687  ssrel2  4822  issref  5126  dmmptg  5241  funco  5373  fununi  5405  fun11uni  5407  funimaexglem  5420  fnmpt  5466  fun11iun  5613  mpteqb  5746  chfnrn  5767  dffo5  5804  ffvresb  5818  fmptcof  5822  dfmptg  5835  mpo2eqb  6141  ralrnmpo  6146  rexrnmpo  6147  uchoice  6309  fnmpo  6376  mpoexxg  6384  smores  6501  riinerm  6820  ixpm  6942  difinfinf  7360  nninfwlpoimlemginf  7435  exmidontriimlem1  7496  onntri13  7516  onntri24  7520  cc4f  7548  cc4n  7550  cauappcvgprlemdisj  7931  caucvgsrlemasr  8070  caucvgsr  8082  suplocsr  8089  rexuz3  11630  recvguniq  11635  cau3lem  11754  caubnd2  11757  rexanre  11860  climi2  11928  climi0  11929  climcaucn  11991  ndvdssub  12571  gcdsupex  12608  gcdsupcl  12609  bezoutlemmo  12657  ptex  13427  mgmidmo  13535  issubg2m  13856  eltg2b  14865  neipsm  14965  lmcvg  15028  txlm  15090  metrest  15317  mulcncflem  15418  wlkvtxeledgg  16285  upgrwlkcompim  16303  upgrwlkvtxedg  16305  upgr2wlkdc  16318  bj-charfunbi  16527  bj-indint  16647  bj-indind  16648  bj-bdfindis  16663  setindis  16683  bdsetindis  16685  pw1dceq  16726  exmidcon  16728  exmidpeirce  16729  neap0mkv  16802