Theorem reximi 2470

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

Syntax hints:   -> wi 4   e. wcel 1438   E.wrex 2360

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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472

This theorem depends on definitions:  df-bi 115  df-ral 2364  df-rex 2365

This theorem is referenced by:  r19.29d2r  2512  r19.35-1  2517  r19.40  2521  reu3  2805  ssiun  3772  iinss  3781  elunirn  5545  tfrcllemssrecs  6117  nnawordex  6287  iinerm  6364  erovlem  6384  xpf1o  6560  fidcenumlemim  6661  genprndl  7080  genprndu  7081  appdiv0nq  7123  ltexprlemm  7159  recexsrlem  7320  rereceu  7424  recexre  8055  rexanre  10653  climi2  10676  climi0  10677  climcaucn  10740  gcdsupex  11227  gcdsupcl  11228  bezoutlemeu  11274  dfgcd3  11277  bj-findis  11874