Theorem eximi 1837

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

Syntax hints:   → wi 4  ∃wex 1781

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

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

This theorem is referenced by:  2eximi  1838  eximii  1839  exa1  1840  exsimpl  1870  exsimpr  1871  19.29r2  1877  19.29x  1878  19.35  1879  19.40-2  1889  emptyex  1909  exlimiv  1932  speimfwALT  1966  nfexhe  2183  19.12  2333  ax13lem2  2381  exdistrf  2452  equs45f  2464  dfmoeu  2536  eu6  2575  2eu2ex  2644  reximi2  3071  cgsexg  3475  gencbvex  3488  eqvincg  3591  sbcg  3802  n0rex  4298  axrep2  5215  sepex  5235  bm1.3iiOLD  5237  ax6vsep  5238  axprg  5374  copsexgw  5438  copsexg  5439  relopabi  5771  dmcoss  5924  dminss  6111  imainss  6112  iotanul2  6465  fv3  6852  ssimaex  6919  dffv2  6929  exfo  7051  oprabidw  7391  oprabid  7392  zfrep6OLD  7901  frxp  8069  suppimacnvss  8116  tz7.48-1  8375  enssdom  8916  enssdomOLD  8917  enfii  9113  fineqvlem  9169  enp1i  9182  infcntss  9226  infeq5  9549  rankuni  9778  scott0  9801  acni3  9960  acnnum  9965  dfac3  10034  dfac9  10050  kmlem1  10064  cflm  10163  cfcof  10187  axdc4lem  10368  axcclem  10370  ac6c4  10394  ac6s  10397  ac6s2  10399  axdclem2  10433  brdom3  10441  brdom5  10442  brdom4  10443  nqpr  10928  ltexprlem4  10953  reclem2pr  10962  hash1to3  14445  trclublem  14948  fnpr2ob  17513  drsdirfi  18262  toprntopon  22900  2ndcsb  23424  fbssint  23813  isfil2  23831  alexsubALTlem3  24024  lpbl  24478  metustfbas  24532  lrrecfr  27949  ex-natded9.26-2  30505  19.9d2rf  32553  rexunirn  32576  f1ocnt  32888  fsumiunle  32917  fmcncfil  34091  esumiun  34254  0elsiga  34274  ddemeas  34396  bnj168  34889  bnj593  34904  bnj607  35074  bnj600  35077  bnj916  35091  axprALT2  35269  fineqvpow  35275  tz9.1regs  35294  onvf1odlem1  35301  wevgblacfn  35307  lfuhgr3  35318  cusgredgex  35320  loop1cycl  35335  umgr2cycl  35339  fundmpss  35965  exisym1  36622  axtco2g  36675  bj-sylge  36917  bj-exextruan  36948  bj-cbvew  36952  bj-19.12  37036  bj-equs45fv  37134  bj-snsetex  37286  bj-snglss  37293  bj-snglex  37296  bj-bm1.3ii  37387  bj-axnul  37395  bj-axseprep  37397  bj-restn0  37418  bj-ccinftydisj  37543  mptsnunlem  37668  pibt2  37747  wl-cbvmotv  37852  wl-moae  37855  wl-nax6im  37857  eu6w  43123  iscard4  43978  ismnushort  44746  spsbce-2  44826  iotaexeu  44863  iotasbc  44864  relopabVD  45345  ax6e2ndeqVD  45353  2uasbanhVD  45355  ax6e2ndeqALT  45375  fnchoice  45478  rfcnnnub  45485  stoweidlem35  46481  stoweidlem57  46503  mo0sn  49303