Theorem eximi 1838

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

Syntax hints:   → wi 4  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2eximi  1839  eximii  1840  exa1  1841  exsimpl  1872  exsimpr  1873  19.29r2  1879  19.29x  1880  19.35  1881  19.40-2  1891  emptyex  1911  exlimiv  1934  speimfwALT  1969  19.12  2321  ax13lem2  2376  exdistrf  2447  equs45f  2459  dfmoeu  2531  moimi  2540  eu6  2569  2eu2ex  2640  reximi2  3080  cgsexg  3519  gencbvex  3536  eqvincg  3637  sbcg  3857  n0rex  4355  axrep2  5289  bm1.3ii  5303  ax6vsep  5304  copsexgw  5491  copsexg  5492  relopabi  5823  dminss  6153  imainss  6154  iotanul2  6514  iotaexOLD  6524  fv3  6910  ssimaex  6977  dffv2  6987  exfo  7107  oprabidw  7440  oprabid  7441  zfrep6  7941  frxp  8112  suppimacnvss  8158  tz7.48-1  8443  enssdom  8973  enfii  9189  fineqvlem  9262  enp1i  9279  infcntss  9321  infeq5  9632  omex  9638  rankuni  9858  scott0  9881  acni3  10042  acnnum  10047  dfac3  10116  dfac9  10131  kmlem1  10145  cflm  10245  cfcof  10269  axdc4lem  10450  axcclem  10452  ac6c4  10476  ac6s  10479  ac6s2  10481  axdclem2  10515  brdom3  10523  brdom5  10524  brdom4  10525  nqpr  11009  ltexprlem4  11034  reclem2pr  11043  hash1to3  14452  trclublem  14942  fnpr2ob  17504  drsdirfi  18258  toprntopon  22427  2ndcsb  22953  fbssint  23342  isfil2  23360  alexsubALTlem3  23553  lpbl  24012  metustfbas  24066  lrrecfr  27427  ex-natded9.26-2  29673  19.9d2rf  31711  rexunirn  31732  f1ocnt  32013  fsumiunle  32035  fmcncfil  32911  esumiun  33092  0elsiga  33112  ddemeas  33234  bnj168  33741  bnj593  33756  bnj607  33927  bnj600  33930  bnj916  33944  fineqvpow  34096  lfuhgr3  34110  cusgredgex  34112  loop1cycl  34128  umgr2cycl  34132  fundmpss  34738  exisym1  35309  bj-sylge  35501  bj-19.12  35639  bj-equs45fv  35689  bj-snsetex  35844  bj-snglss  35851  bj-snglex  35854  bj-bm1.3ii  35945  bj-restn0  35971  bj-ccinftydisj  36094  mptsnunlem  36219  pibt2  36298  wl-cbvmotv  36382  wl-moae  36385  wl-nax6im  36387  iscard4  42284  ismnushort  43060  spsbce-2  43140  iotaexeu  43177  iotasbc  43178  relopabVD  43662  ax6e2ndeqVD  43670  2uasbanhVD  43672  ax6e2ndeqALT  43692  fnchoice  43713  rfcnnnub  43720  stoweidlem35  44751  stoweidlem57  44773  mo0sn  47500