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  2673  reximi2  2720  cgsexg  2890  gencbvex  2901  vtoclf  2908  vtocl3  2911  eqvinc  2966  iotaex  4356  phiall  4618  dmcoss  4971  imassrn  5009  dminss  5041  imainss  5042  fv3  5341  oprabid  5550  nenpw1pwlem2  6085  ncelncs  6120  lecidg  6196  lec0cg  6198  lecncvg  6199  addlec  6208  te0c  6237  dmfrec  6316  fnfrec  6320