Theorem reximi 2458

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

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

Assertion

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

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3 |- ( ph -> ps )
2	1	a1i 9	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	reximia 2456	1 |- ( E. x e. A ph -> E. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1433   E.wrex 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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

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

This theorem is referenced by:  r19.29d2r  2499  r19.35-1  2504  r19.40  2508  reu3  2782  ssiun  3720  iinss  3729  elunirn  5426  nnawordex  6124  iinerm  6201  erovlem  6221  genprndl  6711  genprndu  6712  appdiv0nq  6754  ltexprlemm  6790  recexsrlem  6951  rereceu  7055  recexre  7678  rexanre  10106  climi2  10127  climi0  10128  climcaucn  10188  gcdsupex  10349  gcdsupcl  10350  bezoutlemeu  10396  dfgcd3  10399  bj-findis  10774