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 1801	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4  ∃wex 1783

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

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

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  2325  ax13lem2  2376  exdistrf  2447  equs45f  2459  dfmoeu  2536  moimi  2545  eu6  2574  2eu2ex  2645  reximi2  3171  cgsexg  3464  gencbvex  3478  eqvincg  3570  sbcg  3791  n0rex  4285  axrep2  5208  bm1.3ii  5221  ax6vsep  5222  copsexgw  5398  copsexg  5399  relopabi  5721  dminss  6045  imainss  6046  iotaex  6398  fv3  6774  ssimaex  6835  dffv2  6845  exfo  6963  oprabidw  7286  oprabid  7287  zfrep6  7771  frxp  7938  suppimacnvss  7960  tz7.48-1  8244  enssdom  8720  enfii  8932  fineqvlem  8966  infcntss  9018  infeq5  9325  omex  9331  rankuni  9552  scott0  9575  acni3  9734  acnnum  9739  dfac3  9808  dfac9  9823  kmlem1  9837  cflm  9937  cfcof  9961  axdc4lem  10142  axcclem  10144  ac6c4  10168  ac6s  10171  ac6s2  10173  axdclem2  10207  brdom3  10215  brdom5  10216  brdom4  10217  nqpr  10701  ltexprlem4  10726  reclem2pr  10735  hash1to3  14133  trclublem  14634  fnpr2ob  17186  drsdirfi  17938  toprntopon  21982  2ndcsb  22508  fbssint  22897  isfil2  22915  alexsubALTlem3  23108  lpbl  23565  metustfbas  23619  ex-natded9.26-2  28685  19.9d2rf  30721  rexunirn  30741  f1ocnt  31025  fsumiunle  31045  fmcncfil  31783  esumiun  31962  0elsiga  31982  ddemeas  32104  bnj168  32609  bnj593  32625  bnj607  32796  bnj600  32799  bnj916  32813  fineqvpow  32965  lfuhgr3  32981  cusgredgex  32983  loop1cycl  32999  umgr2cycl  33003  fundmpss  33646  lrrecfr  34027  exisym1  34540  bj-sylge  34732  bj-19.12  34870  bj-equs45fv  34920  bj-snsetex  35080  bj-snglss  35087  bj-snglex  35090  bj-bm1.3ii  35162  bj-restn0  35188  bj-ccinftydisj  35311  mptsnunlem  35436  pibt2  35515  wl-cbvmotv  35599  wl-moae  35602  wl-nax6im  35604  sn-iotanul  40121  iscard4  41038  ismnushort  41808  spsbce-2  41888  iotaexeu  41925  iotasbc  41926  relopabVD  42410  ax6e2ndeqVD  42418  2uasbanhVD  42420  ax6e2ndeqALT  42440  fnchoice  42461  rfcnnnub  42468  stoweidlem35  43466  stoweidlem57  43488  mo0sn  46049