Theorem ralimi 2607

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

Syntax hints:   -> wi 4   e. wcel 2205   A.wral 2522

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 2527

This theorem is referenced by:  2ralimi  2608  ral2imi  2609  r19.26  2671  r19.29  2682  rr19.3v  2959  rr19.28v  2960  reu3  3010  uniiunlem  3332  reupick2  3511  rabxmdc  3544  uniss2  3950  ss2iun  4011  iineq2  4013  iunss2  4041  disjss2  4093  disjeq2  4094  disjnim  4104  repizf  4231  abnexg  4572  reusv3i  4585  tfis  4710  ssrel2  4845  issref  5150  dmmptg  5265  funco  5397  fununi  5429  fun11uni  5431  funimaexglem  5444  fnmpt  5490  fun11iun  5640  mpteqb  5773  chfnrn  5794  dffo5  5831  ffvresb  5845  fmptcof  5849  dfmptg  5862  mpo2eqb  6171  ralrnmpo  6176  rexrnmpo  6177  uchoice  6344  fnmpo  6411  mpoexxg  6419  smores  6536  riinerm  6855  ixpm  6978  difinfinf  7405  nninfwlpoimlemginf  7480  exmidontriimlem1  7541  onntri13  7561  onntri24  7565  cc4f  7599  cc4n  7601  cauappcvgprlemdisj  7982  caucvgsrlemasr  8121  caucvgsr  8133  suplocsr  8140  rexuz3  11700  recvguniq  11705  cau3lem  11824  caubnd2  11827  rexanre  11930  climi2  11998  climi0  11999  climcaucn  12061  ndvdssub  12641  gcdsupex  12678  gcdsupcl  12679  bezoutlemmo  12727  ptex  13561  mgmidmo  13635  issubg2m  13942  eltg2b  15045  neipsm  15145  lmcvg  15208  txlm  15270  metrest  15497  mulcncflem  15598  wlkvtxeledgg  16465  upgrwlkcompim  16483  upgrwlkvtxedg  16485  upgr2wlkdc  16498  bj-charfunbi  16707  bj-indint  16827  bj-indind  16828  bj-bdfindis  16843  setindis  16863  bdsetindis  16865  pw1dceq  16904  exmidcon  16906  exmidpeirce  16907  neap0mkv  16981