Theorem eximi 1576

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

Hypothesis

Ref	Expression
eximi.1	⊢ (φ → ψ)

Assertion

Ref	Expression
eximi	⊢ (∃xφ → ∃xψ)

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1575	. 2 ⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ))
2		eximi.1	. 2 ⊢ (φ → ψ)
3	1, 2	mpg 1548	1 ⊢ (∃xφ → ∃xψ)

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  2eximi  1577  exsimpl  1592  19.29r2  1598  19.29x  1599  19.40  1609  19.40-2  1610  exlimiv  1634  speimfw  1645  sbimi  1652  exiftru  1657  spimeh  1667  equid  1676  exlimivOLD  1698  19.12  1847  19.12OLD  1848  cbv3hv  1850  equs4  1959  exdistrf  1971  equvini  1987  equs45f  1989  sbequi  2059  eumo0  2228  euan  2261  eupickb  2269  2eu2ex  2278  darii  2303  barbari  2305  festino  2309  baroco  2310  cesaro  2311  camestros  2312  datisi  2313  disamis  2314  felapton  2317  darapti  2318  dimatis  2320  fresison  2321  calemos  2322  fesapo  2323  bamalip  2324  rexex  2674  reximi2  2721  cgsexg  2891  gencbvex  2902  vtoclf  2909  vtocl3  2912  eqvinc  2967  iotaex  4357  phiall  4619  dmcoss  4972  imassrn  5010  dminss  5042  imainss  5043  fv3  5342  oprabid  5551  nenpw1pwlem2  6086  ncelncs  6121  lecidg  6197  lec0cg  6199  lecncvg  6200  addlec  6209  te0c  6238  dmfrec  6317  fnfrec  6321