Theorem eximi 1835

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

Syntax hints:   → wi 4  ∃wex 1779

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

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

This theorem is referenced by:  2eximi  1836  eximii  1837  exa1  1838  exsimpl  1868  exsimpr  1869  19.29r2  1875  19.29x  1876  19.35  1877  19.40-2  1887  emptyex  1907  exlimiv  1930  speimfwALT  1964  19.12  2326  ax13lem2  2375  exdistrf  2446  equs45f  2458  dfmoeu  2530  moimi  2539  eu6  2568  2eu2ex  2637  reximi2  3063  cgsexg  3495  gencbvex  3510  eqvincg  3617  sbcg  3829  n0rex  4323  axrep2  5240  sepex  5258  bm1.3iiOLD  5260  ax6vsep  5261  copsexgw  5453  copsexg  5454  relopabi  5788  dminss  6129  imainss  6130  iotanul2  6484  iotaexOLD  6494  fv3  6879  ssimaex  6949  dffv2  6959  exfo  7080  oprabidw  7421  oprabid  7422  zfrep6  7936  frxp  8108  suppimacnvss  8155  tz7.48-1  8414  enssdom  8951  enfii  9156  fineqvlem  9216  enp1i  9231  infcntss  9280  infeq5  9597  rankuni  9823  scott0  9846  acni3  10007  acnnum  10012  dfac3  10081  dfac9  10097  kmlem1  10111  cflm  10210  cfcof  10234  axdc4lem  10415  axcclem  10417  ac6c4  10441  ac6s  10444  ac6s2  10446  axdclem2  10480  brdom3  10488  brdom5  10489  brdom4  10490  nqpr  10974  ltexprlem4  10999  reclem2pr  11008  hash1to3  14464  trclublem  14968  fnpr2ob  17528  drsdirfi  18273  toprntopon  22819  2ndcsb  23343  fbssint  23732  isfil2  23750  alexsubALTlem3  23943  lpbl  24398  metustfbas  24452  lrrecfr  27857  ex-natded9.26-2  30356  19.9d2rf  32405  rexunirn  32428  f1ocnt  32732  fsumiunle  32761  fmcncfil  33928  esumiun  34091  0elsiga  34111  ddemeas  34233  bnj168  34727  bnj593  34742  bnj607  34913  bnj600  34916  bnj916  34930  fineqvpow  35093  onvf1odlem1  35097  wevgblacfn  35103  lfuhgr3  35114  cusgredgex  35116  loop1cycl  35131  umgr2cycl  35135  fundmpss  35761  exisym1  36419  bj-sylge  36619  bj-19.12  36756  bj-equs45fv  36806  bj-snsetex  36958  bj-snglss  36965  bj-snglex  36968  bj-bm1.3ii  37059  bj-restn0  37085  bj-ccinftydisj  37208  mptsnunlem  37333  pibt2  37412  wl-cbvmotv  37508  wl-moae  37511  wl-nax6im  37513  eu6w  42671  iscard4  43529  ismnushort  44297  spsbce-2  44377  iotaexeu  44414  iotasbc  44415  relopabVD  44897  ax6e2ndeqVD  44905  2uasbanhVD  44907  ax6e2ndeqALT  44927  fnchoice  45030  rfcnnnub  45037  stoweidlem35  46040  stoweidlem57  46062  mo0sn  48808