Theorem eximi 1600

Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
eximi	|- ( E. x ph -> E. x ps )

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1599	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		eximi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1451	1 |- ( E. x ph -> E. x ps )

Syntax hints:   -> wi 4   E.wex 1492

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1601  eximii  1602  exsimpl  1617  exsimpr  1618  19.29r2  1622  19.29x  1623  19.35-1  1624  19.43  1628  19.40  1631  19.40-2  1632  exanaliim  1647  19.12  1665  equs4  1725  cbvexh  1755  equvini  1758  sbimi  1764  equs5e  1795  exdistrfor  1800  equs45f  1802  sbcof2  1810  sbequi  1839  spsbe  1842  sbidm  1851  cbvexdh  1926  eumo0  2057  mor  2068  euan  2082  eupickb  2107  2eu2ex  2115  2exeu  2118  rexex  2523  reximi2  2573  cgsexg  2772  gencbvex  2783  gencbval  2785  vtocl3  2793  eqvinc  2860  eqvincg  2861  mosubt  2914  rexm  3522  prmg  3712  bm1.3ii  4121  a9evsep  4122  axnul  4125  elrelimasn  4990  dminss  5039  imainss  5040  euiotaex  5190  imadiflem  5291  funimaexglem  5295  brprcneu  5504  fv3  5534  relelfvdm  5543  ssimaex  5573  oprabid  5901  brabvv  5915  ecexr  6534  enssdom  6756  fidcenumlemim  6945  subhalfnqq  7401  prarloc  7490  ltexprlemopl  7588  ltexprlemlol  7589  ltexprlemopu  7590  ltexprlemupu  7591  bdbm1.3ii  14292  bj-inex  14308  bj-2inf  14339