Theorem eximi 1738

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

Hypothesis

Ref	Expression
eximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
eximi	⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1737	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		eximi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1700	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711

This theorem depends on definitions:  df-bi 192  df-ex 1693

This theorem is referenced by:  2eximi  1739  eximii  1740  exa1  1742  exsimpl  1760  exsimpr  1761  19.29r2  1769  19.29x  1770  19.35  1771  19.40-2  1780  exlimiv  1807  speimfwALT  1825  sbimi  1834  19.12  2085  ax13lem2  2180  axc9lem2OLD  2181  exdistrf  2216  equs45f  2233  mo2v  2360  2eu2ex  2429  reximi2  2886  cgsexg  3101  gencbvex  3113  vtocl3  3124  eqvinc  3189  axrep2  4550  bm1.3ii  4561  ax6vsep  4562  axnulOLD  4566  copsexg  4728  dminss  5300  imainss  5301  elsnxp  5429  iotaex  5614  fv3  5940  ssimaex  5997  dffv2  6005  exfo  6107  oprabid  6390  zfrep6  6838  frxp  6985  suppimacnvss  7003  tz7.48-1  7237  enssdom  7677  fineqvlem  7870  infcntss  7930  infeq5  8227  omex  8233  rankuni  8419  scott0  8442  acni3  8563  acnnum  8568  dfac3  8637  dfac9  8651  kmlem1  8665  cflm  8765  cfcof  8789  axdc4lem  8970  axcclem  8972  ac6c4  8996  ac6s  8999  ac6s2  9001  axdclem2  9035  brdom3  9041  brdom5  9042  brdom4  9043  nqpr  9524  ltexprlem4  9549  reclem2pr  9558  hash1to3  12771  trclublem  13217  drsdirfi  16349  2ndcsb  20621  fbssint  21011  isfil2  21029  alexsubALTlem3  21222  lpbl  21676  metustfbas  21730  3v3e3cycl2  25553  ex-natded9.26-2  26030  eqvincg  28271  19.9d2rf  28275  rexunirn  28288  f1ocnt  28532  fmcncfil  28892  esumiun  29070  0elsiga  29091  ddemeas  29213  bnj168  29691  bnj593  29708  bnj607  29879  bnj600  29882  bnj916  29896  fundmpss  30558  exisym1  31233  bj-exlime  31402  bj-nalnaleximiOLD  31404  bj-sbex  31421  bj-ssbequ2  31438  bj-equs45fv  31544  bj-axrep2  31586  bj-eumo0  31627  bj-snsetex  31743  bj-snglss  31750  bj-snglex  31753  bj-restn0  31823  bj-toprntopon  31843  bj-ccinftydisj  31876  mptsnunlem  31961  spsbce-2  37087  iotaexeu  37126  iotasbc  37127  relopabVD  37646  ax6e2ndeqVD  37654  2uasbanhVD  37656  ax6e2ndeqALT  37676  fnchoice  37698  rfcnnnub  37705  stoweidlem35  38332  stoweidlem57  38354  n0rex  39510