Theorem eximi 1832

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

Syntax hints:   → wi 4  ∃wex 1776

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

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

This theorem is referenced by:  2eximi  1833  eximii  1834  exa1  1835  exsimpl  1866  exsimpr  1867  19.29r2  1873  19.29x  1874  19.35  1875  19.40-2  1885  emptyex  1905  exlimiv  1928  speimfwALT  1962  19.12  2326  ax13lem2  2379  exdistrf  2450  equs45f  2462  dfmoeu  2534  moimi  2543  eu6  2572  2eu2ex  2641  reximi2  3077  cgsexg  3524  gencbvex  3541  eqvincg  3648  sbcg  3870  n0rex  4363  axrep2  5288  sepex  5306  bm1.3iiOLD  5308  ax6vsep  5309  copsexgw  5501  copsexg  5502  relopabi  5835  dminss  6175  imainss  6176  iotanul2  6533  iotaexOLD  6543  fv3  6925  ssimaex  6994  dffv2  7004  exfo  7125  oprabidw  7462  oprabid  7463  zfrep6  7978  frxp  8150  suppimacnvss  8197  tz7.48-1  8482  enssdom  9016  enfii  9224  fineqvlem  9296  enp1i  9311  infcntss  9360  infeq5  9675  omex  9681  rankuni  9901  scott0  9924  acni3  10085  acnnum  10090  dfac3  10159  dfac9  10175  kmlem1  10189  cflm  10288  cfcof  10312  axdc4lem  10493  axcclem  10495  ac6c4  10519  ac6s  10522  ac6s2  10524  axdclem2  10558  brdom3  10566  brdom5  10567  brdom4  10568  nqpr  11052  ltexprlem4  11077  reclem2pr  11086  hash1to3  14528  trclublem  15031  fnpr2ob  17605  drsdirfi  18363  toprntopon  22947  2ndcsb  23473  fbssint  23862  isfil2  23880  alexsubALTlem3  24073  lpbl  24532  metustfbas  24586  lrrecfr  27991  ex-natded9.26-2  30449  19.9d2rf  32498  rexunirn  32520  f1ocnt  32810  fsumiunle  32836  fmcncfil  33892  esumiun  34075  0elsiga  34095  ddemeas  34217  bnj168  34723  bnj593  34738  bnj607  34909  bnj600  34912  bnj916  34926  fineqvpow  35089  wevgblacfn  35093  lfuhgr3  35104  cusgredgex  35106  loop1cycl  35122  umgr2cycl  35126  fundmpss  35748  exisym1  36407  bj-sylge  36607  bj-19.12  36744  bj-equs45fv  36794  bj-snsetex  36946  bj-snglss  36953  bj-snglex  36956  bj-bm1.3ii  37047  bj-restn0  37073  bj-ccinftydisj  37196  mptsnunlem  37321  pibt2  37400  wl-cbvmotv  37494  wl-moae  37497  wl-nax6im  37499  eu6w  42663  iscard4  43523  ismnushort  44297  spsbce-2  44377  iotaexeu  44414  iotasbc  44415  relopabVD  44899  ax6e2ndeqVD  44907  2uasbanhVD  44909  ax6e2ndeqALT  44929  fnchoice  44967  rfcnnnub  44974  stoweidlem35  45991  stoweidlem57  46013  mo0sn  48664