Theorem eximi 1834

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 1833	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		eximi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1796	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1778

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

This theorem depends on definitions:  df-bi 207  df-ex 1779

This theorem is referenced by:  2eximi  1835  eximii  1836  exa1  1837  exsimpl  1867  exsimpr  1868  19.29r2  1874  19.29x  1875  19.35  1876  19.40-2  1886  emptyex  1906  exlimiv  1929  speimfwALT  1963  19.12  2326  ax13lem2  2380  exdistrf  2451  equs45f  2463  dfmoeu  2535  moimi  2544  eu6  2573  2eu2ex  2642  reximi2  3078  cgsexg  3525  gencbvex  3540  eqvincg  3647  sbcg  3862  n0rex  4356  axrep2  5281  sepex  5299  bm1.3iiOLD  5301  ax6vsep  5302  copsexgw  5494  copsexg  5495  relopabi  5831  dminss  6172  imainss  6173  iotanul2  6530  iotaexOLD  6540  fv3  6923  ssimaex  6993  dffv2  7003  exfo  7124  oprabidw  7463  oprabid  7464  zfrep6  7980  frxp  8152  suppimacnvss  8199  tz7.48-1  8484  enssdom  9018  enfii  9227  fineqvlem  9299  enp1i  9314  infcntss  9363  infeq5  9678  rankuni  9904  scott0  9927  acni3  10088  acnnum  10093  dfac3  10162  dfac9  10178  kmlem1  10192  cflm  10291  cfcof  10315  axdc4lem  10496  axcclem  10498  ac6c4  10522  ac6s  10525  ac6s2  10527  axdclem2  10561  brdom3  10569  brdom5  10570  brdom4  10571  nqpr  11055  ltexprlem4  11080  reclem2pr  11089  hash1to3  14532  trclublem  15035  fnpr2ob  17604  drsdirfi  18352  toprntopon  22932  2ndcsb  23458  fbssint  23847  isfil2  23865  alexsubALTlem3  24058  lpbl  24517  metustfbas  24571  lrrecfr  27977  ex-natded9.26-2  30440  19.9d2rf  32489  rexunirn  32512  f1ocnt  32805  fsumiunle  32832  fmcncfil  33931  esumiun  34096  0elsiga  34116  ddemeas  34238  bnj168  34745  bnj593  34760  bnj607  34931  bnj600  34934  bnj916  34948  fineqvpow  35111  wevgblacfn  35115  lfuhgr3  35126  cusgredgex  35128  loop1cycl  35143  umgr2cycl  35147  fundmpss  35768  exisym1  36426  bj-sylge  36626  bj-19.12  36763  bj-equs45fv  36813  bj-snsetex  36965  bj-snglss  36972  bj-snglex  36975  bj-bm1.3ii  37066  bj-restn0  37092  bj-ccinftydisj  37215  mptsnunlem  37340  pibt2  37419  wl-cbvmotv  37515  wl-moae  37518  wl-nax6im  37520  eu6w  42691  iscard4  43551  ismnushort  44325  spsbce-2  44405  iotaexeu  44442  iotasbc  44443  relopabVD  44926  ax6e2ndeqVD  44934  2uasbanhVD  44936  ax6e2ndeqALT  44956  fnchoice  45039  rfcnnnub  45046  stoweidlem35  46055  stoweidlem57  46077  mo0sn  48740